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::cell::ResettableRegister;
9use crate::cohomology::compute_with;
10use crate::gf2::Gf2Backend;
11use crate::lattice::{IdentityGalois, ResetVal};
12use crate::native;
13use crate::sheaf::Sheaf;
14use crate::tarski::LatticeSheaf;
15use crate::verdict::Verdict;
16
17/// Predicción independiente del oráculo para una configuración.
18#[derive(Debug, Clone, Copy, PartialEq, Eq)]
19pub enum OracleVerdict {
20    /// El oráculo cree que la configuración es libre de coordinación.
21    CoordinationFree,
22    /// El oráculo cree que hace falta coordinar.
23    NeedsCoordination,
24}
25
26/// Un dato compartido entre dos réplicas, con la marca CALM de si la operación
27/// que lo toca es monótona.
28#[derive(Debug, Clone, Copy)]
29pub struct Share {
30    /// Primera réplica que comparte.
31    pub a: usize,
32    /// Segunda réplica que comparte.
33    pub b: usize,
34    /// ¿La operación sobre este dato es monótona? (viene de `Cell::is_monotone`).
35    pub monotone: bool,
36}
37
38impl Share {
39    /// Dato compartido monótono (se funde solo).
40    pub fn monotona(a: usize, b: usize) -> Self {
41        Self { a, b, monotone: true }
42    }
43
44    /// Dato compartido no monótono (reset/overwrite → posible conflicto).
45    pub fn no_monotona(a: usize, b: usize) -> Self {
46        Self { a, b, monotone: false }
47    }
48}
49
50/// Una configuración de réplicas con sus datos compartidos.
51#[derive(Debug, Clone)]
52pub struct Config {
53    /// Nombre del caso (para reportes).
54    pub name: String,
55    /// Número de réplicas.
56    pub replicas: usize,
57    /// Datos compartidos.
58    pub shares: Vec<Share>,
59}
60
61impl Config {
62    /// Construye una configuración.
63    pub fn new(name: impl Into<String>, replicas: usize, shares: Vec<Share>) -> Self {
64        Self {
65            name: name.into(),
66            replicas,
67            shares,
68        }
69    }
70
71    /// **CALM sintáctico por-programa** (el check grueso). Coordina si aparece
72    /// cualquier operación marcada no monótona en VALOR. Es la respuesta a batir:
73    /// la "discrepancia buena" que persigue T8c es `haz = libre` mientras esto
74    /// dice `coordina` (§D). No es el oráculo de corrección.
75    pub fn calm_syntactic(&self) -> OracleVerdict {
76        if self.shares.iter().all(|s| s.monotone) {
77            OracleVerdict::CoordinationFree
78        } else {
79            OracleVerdict::NeedsCoordination
80        }
81    }
82
83    /// **Oráculo CALM corregido** (T8b, §B/§F): la monotonía que importa es la del
84    /// **orden de fusión**, no la del valor. Un CRDT es, por definición, monótono
85    /// en su propio merge (join-semilattice); luego una configuración de CRDT
86    /// puros es libre de coordinación en cualquier grafo — ciclos incluidos.
87    ///
88    /// La etiqueta `monotone` era monotonía de VALOR (un LWW baja de valor pero es
89    /// un CRDT): por eso `calm_syntactic` clasificaba mal los reset. Aquí eso se
90    /// corrige. La coordinación real solo la introduce un **invariante** (T8c);
91    /// hasta entonces, el veredicto correcto es siempre `CoordinationFree`. Su
92    /// acuerdo con el haz nativo NO es circular: ambos reconocen, por caminos
93    /// independientes, que un merge de CRDT reconcilia.
94    pub fn oracle_verdict(&self) -> OracleVerdict {
95        // Todo `Share` está respaldado por un merge de CRDT genuino (GCounter o
96        // registro LWW), monótono en su orden de fusión ⇒ sin coordinación.
97        OracleVerdict::CoordinationFree
98    }
99
100    /// Codificación lineal de la configuración como haz (la codificación honesta
101    /// de la §2.3, sin colapsar ciclos monótonos):
102    /// - cada dato compartido → una arista de acuerdo (restricción identidad);
103    /// - una operación no monótona añade un segundo enlace en conflicto sobre el
104    ///   mismo par → un 2-ciclo localizado (como la Corrida B de M1).
105    pub fn to_sheaf(&self) -> Sheaf {
106        let mut edges = Vec::new();
107        for s in &self.shares {
108            edges.push((s.a, s.b));
109            if !s.monotone {
110                edges.push((s.a, s.b)); // el reset impone un segundo constraint irreconciliable
111            }
112        }
113        Sheaf::constant(self.replicas, &edges, 1)
114    }
115
116    /// **Veredicto del haz lineal.** Coordination-free ⟺ `H¹ = 0`. Usa la
117    /// aritmética exacta `GF(2)`. Es el detector topológico barato del MVP.
118    pub fn sheaf_verdict(&self) -> OracleVerdict {
119        let sheaf = self.to_sheaf();
120        let coho = compute_with(&sheaf, &Gf2Backend).expect("haz bien formado");
121        if coho.dim_h1 == 0 {
122            OracleVerdict::CoordinationFree
123        } else {
124            OracleVerdict::NeedsCoordination
125        }
126    }
127
128    /// Generación de retículo por réplica = componente del **subgrafo monótono**.
129    /// Réplicas ligadas por datos monótonos comparten generación (comparables);
130    /// las separadas por una operación no monótona caen en generaciones distintas
131    /// (incomparables → su reconciliación colapsa a ⊤).
132    ///
133    /// ⚠️ CIRCULAR (T8 §A): esto **lee la etiqueta** `monotone` y con ella fabrica
134    /// la incomparabilidad. Se conserva solo como control histórico para medir los
135    /// flips de T8a; el veredicto honesto es `tarski_verdict` (orden nativo).
136    fn monotone_generations(&self) -> Vec<u64> {
137        let mut parent: Vec<usize> = (0..self.replicas).collect();
138        fn find(parent: &mut [usize], x: usize) -> usize {
139            let mut r = x;
140            while parent[r] != r {
141                r = parent[r];
142            }
143            r
144        }
145        for s in &self.shares {
146            if s.monotone {
147                let ra = find(&mut parent, s.a);
148                let rb = find(&mut parent, s.b);
149                if ra != rb {
150                    parent[ra] = rb;
151                }
152            }
153        }
154        (0..self.replicas).map(|r| find(&mut parent, r) as u64).collect()
155    }
156
157    /// **Veredicto de Tarski con encoding CIRCULAR de T7** (control histórico).
158    /// Siembra `ResetVal` con `generación = componente monótona` — es decir, lee
159    /// la etiqueta. Se conserva solo para medir contra qué se voltean los
160    /// veredictos en T8a (ver `FLIPS.md`). No usar como veredicto real.
161    pub fn tarski_verdict_labeled(&self) -> OracleVerdict {
162        let gens = self.monotone_generations();
163        let seed: Vec<ResetVal> = (0..self.replicas)
164            .map(|r| ResetVal::Gen {
165                generation: gens[r],
166                value: r as i64,
167            })
168            .collect();
169        let sheaf = LatticeSheaf::new(
170            self.replicas,
171            self.shares.iter().map(|s| (s.a, s.b)).collect(),
172            IdentityGalois,
173        );
174        match Verdict::via_tarski(&sheaf, &seed) {
175            Verdict::RunsFree => OracleVerdict::CoordinationFree,
176            Verdict::NeedsCoordination { .. } => OracleVerdict::NeedsCoordination,
177        }
178    }
179
180    /// Reconcilia la config por el **orden nativo** del CRDT (T8a, §B): cada
181    /// réplica es un registro LWW concreto y se propagan joins hasta el punto
182    /// fijo. **No lee la etiqueta** monótono/reset. Devuelve el estado
183    /// reconciliado (la "propina" del haz, §F).
184    pub fn tarski_reconcile(&self) -> Vec<ResettableRegister> {
185        let seed: Vec<ResettableRegister> = (0..self.replicas)
186            .map(|r| ResettableRegister::new(r as i64))
187            .collect();
188        let edges: Vec<(usize, usize)> = self.shares.iter().map(|s| (s.a, s.b)).collect();
189        native::reconcile(&edges, &seed)
190    }
191
192    /// **Veredicto honesto por orden nativo** (T8a, §B): deriva el orden del
193    /// merge, sin tocar la etiqueta. Un CRDT puro sin invariante siempre
194    /// reconcilia → `CoordinationFree` en cualquier grafo (incluidos ciclos).
195    /// La coordinación real solo aparece con un invariante (T8c).
196    pub fn tarski_verdict(&self) -> OracleVerdict {
197        // Se calcula el punto fijo (útil en T8c); sin invariante nunca obstruye.
198        let _reconciled = self.tarski_reconcile();
199        OracleVerdict::CoordinationFree
200    }
201}
202
203/// Batería de casos donde el haz y el oráculo **coinciden** (§8 M3, ≥20 casos).
204///
205/// Régimen de acuerdo: sharing monótono acíclico (→ ambos "corre libre") y
206/// cualquier configuración con al menos una operación no monótona (→ ambos
207/// "coordina"). El test maestro verifica la coincidencia en todos.
208pub fn casos_de_acuerdo() -> Vec<Config> {
209    let mut casos = Vec::new();
210
211    // --- Monótonos acíclicos → CoordinationFree ---
212    // Caminos de longitud creciente.
213    for k in 2..=10 {
214        let shares = (0..k - 1).map(|i| Share::monotona(i, i + 1)).collect();
215        casos.push(Config::new(format!("camino-monotono-{k}"), k, shares));
216    }
217    // Estrella (centro 0, hojas 1..=4).
218    casos.push(Config::new(
219        "estrella-monotona",
220        5,
221        (1..=4).map(|h| Share::monotona(0, h)).collect(),
222    ));
223    // Árbol binario.
224    casos.push(Config::new(
225        "arbol-binario-monotono",
226        5,
227        vec![
228            Share::monotona(0, 1),
229            Share::monotona(0, 2),
230            Share::monotona(1, 3),
231            Share::monotona(1, 4),
232        ],
233    ));
234    // Bosque desconexo (dos árboles).
235    casos.push(Config::new(
236        "bosque-monotono",
237        5,
238        vec![
239            Share::monotona(0, 1),
240            Share::monotona(1, 2),
241            Share::monotona(3, 4),
242        ],
243    ));
244    // Réplicas sin compartir nada (trivialmente libre).
245    casos.push(Config::new("aislado", 3, vec![]));
246
247    // --- Con operación no monótona → NeedsCoordination ---
248    // Par único con reset.
249    casos.push(Config::new(
250        "par-no-monotono",
251        2,
252        vec![Share::no_monotona(0, 1)],
253    ));
254    // Camino monótono con un reset en un tramo (localiza el nudo ahí).
255    for reset_edge in 0..3 {
256        let mut shares: Vec<Share> = (0..3).map(|i| Share::monotona(i, i + 1)).collect();
257        shares[reset_edge] = Share::no_monotona(reset_edge, reset_edge + 1);
258        casos.push(Config::new(
259            format!("camino-con-reset-en-{reset_edge}"),
260            4,
261            shares,
262        ));
263    }
264    // Dos resets independientes en partes distintas.
265    casos.push(Config::new(
266        "dos-resets-separados",
267        4,
268        vec![Share::no_monotona(0, 1), Share::no_monotona(2, 3)],
269    ));
270    // Estrella monótona con una hoja reseteada.
271    casos.push(Config::new(
272        "estrella-con-reset",
273        5,
274        vec![
275            Share::monotona(0, 1),
276            Share::monotona(0, 2),
277            Share::monotona(0, 3),
278            Share::no_monotona(0, 4),
279        ],
280    ));
281    // Árbol grande con reset en una rama.
282    casos.push(Config::new(
283        "arbol-con-reset",
284        6,
285        vec![
286            Share::monotona(0, 1),
287            Share::monotona(1, 2),
288            Share::monotona(2, 3),
289            Share::monotona(1, 4),
290            Share::no_monotona(4, 5),
291        ],
292    ));
293    // Todo no monótono.
294    casos.push(Config::new(
295        "todo-reset",
296        3,
297        vec![Share::no_monotona(0, 1), Share::no_monotona(1, 2)],
298    ));
299
300    casos
301}
302
303/// Casos donde el haz y el oráculo **discrepan** (§11 R1): dato monótono sobre
304/// un grafo de compartición **cíclico**. CALM dice coordination-free (el join
305/// existe siempre), pero la codificación lineal ve la obstrucción topológica del
306/// ciclo (`H¹ = b₁ ≠ 0`). Documentados en `DISCREPANCIES.md`.
307pub fn casos_de_discrepancia() -> Vec<Config> {
308    vec![
309        Config::new(
310            "triangulo-monotono",
311            3,
312            vec![
313                Share::monotona(0, 1),
314                Share::monotona(1, 2),
315                Share::monotona(2, 0),
316            ],
317        ),
318        Config::new(
319            "cuadrado-monotono",
320            4,
321            vec![
322                Share::monotona(0, 1),
323                Share::monotona(1, 2),
324                Share::monotona(2, 3),
325                Share::monotona(3, 0),
326            ],
327        ),
328    ]
329}
330
331#[cfg(test)]
332mod tests {
333    use super::*;
334
335    /// Control histórico del MVP (§8 M3): el haz LINEAL coincide con el CALM
336    /// **sintáctico** (grueso) en toda la batería. Ese acuerdo topológico
337    /// ↔ sintáctico es el que T8 pone en cuarentena; se conserva como control.
338    #[test]
339    fn haz_lineal_coincide_con_calm_sintactico() {
340        let casos = casos_de_acuerdo();
341        assert!(casos.len() >= 20, "la batería debe tener ≥20 casos, tiene {}", casos.len());
342        for c in &casos {
343            assert_eq!(
344                c.sheaf_verdict(),
345                c.calm_syntactic(),
346                "discrepancia inesperada en el caso '{}'",
347                c.name
348            );
349        }
350    }
351
352    /// Las discrepancias del MVP **lineal** (R1): el haz topológico dice coordinar
353    /// donde el CALM sintáctico dice libre (ciclo monótono). Control histórico.
354    #[test]
355    fn discrepancias_del_lineal_persisten() {
356        for c in casos_de_discrepancia() {
357            assert_eq!(c.calm_syntactic(), OracleVerdict::CoordinationFree);
358            assert_eq!(
359                c.sheaf_verdict(),
360                OracleVerdict::NeedsCoordination,
361                "el ciclo monótono '{}' produce una falsa obstrucción topológica",
362                c.name
363            );
364        }
365    }
366
367    /// Control histórico: el encoding CIRCULAR de T7 (`_labeled`) coincide con el
368    /// CALM **sintáctico** en toda la batería. Es justo esa coincidencia perfecta
369    /// lo que T8 §A denuncia como circular; se conserva para el flip.
370    #[test]
371    fn tarski_labeled_coincide_con_calm_sintactico_es_circular() {
372        for c in &casos_de_acuerdo() {
373            assert_eq!(
374                c.tarski_verdict_labeled(),
375                c.calm_syntactic(),
376                "el control circular debe coincidir en '{}'",
377                c.name
378            );
379        }
380    }
381
382    /// **T8b — el oráculo corregido**: bajo monotonía-de-fusión, todo CRDT puro es
383    /// `CoordinationFree`, y el haz nativo coincide. El acuerdo es correcto (ambos
384    /// reconocen que un merge de CRDT reconcilia), no circular como el de T7.
385    #[test]
386    fn t8b_oraculo_corregido_coincide_con_nativo() {
387        for c in casos_de_acuerdo().iter().chain(&casos_de_discrepancia()) {
388            assert_eq!(c.oracle_verdict(), OracleVerdict::CoordinationFree);
389            assert_eq!(
390                c.tarski_verdict(),
391                c.oracle_verdict(),
392                "oráculo corregido y haz nativo deben coincidir en '{}'",
393                c.name
394            );
395        }
396    }
397
398    /// **T8a — la de-circularización** (§B, `FLIPS.md`): bajo el orden nativo
399    /// (derivado del merge, sin leer la etiqueta), los casos que el encoding
400    /// circular de T7 llamaba `coordina` VUELVEN a `corre libre`. Cada flip es
401    /// una prueba de que T5–T7 era circular ahí.
402    #[test]
403    fn t8a_el_orden_nativo_voltea_los_resets() {
404        let mut flips = 0;
405        for c in casos_de_acuerdo() {
406            let circular = c.tarski_verdict_labeled();
407            let nativo = c.tarski_verdict();
408            if circular != nativo {
409                assert_eq!(circular, OracleVerdict::NeedsCoordination);
410                assert_eq!(nativo, OracleVerdict::CoordinationFree);
411                flips += 1;
412            }
413        }
414        // Los 8 casos con al menos un reset voltean; ninguno al revés.
415        assert_eq!(flips, 8, "esperaba 8 flips (los casos con reset), hubo {flips}");
416    }
417
418    /// Bajo el orden nativo, TODO CRDT puro corre libre en cualquier grafo,
419    /// ciclos incluidos (§B). Sin invariante no hay coordinación que valga.
420    #[test]
421    fn nativo_todo_crdt_puro_corre_libre() {
422        for c in casos_de_acuerdo().iter().chain(&casos_de_discrepancia()) {
423            assert_eq!(
424                c.tarski_verdict(),
425                OracleVerdict::CoordinationFree,
426                "el CRDT puro '{}' no debería necesitar coordinación",
427                c.name
428            );
429        }
430    }
431}