tawasuyu/hifas

1//! Invariantes basadas en propiedades (§9), que `proptest` intenta romper.
2//!
3//! Tres invariantes:
4//! 1. Solo-suma (monótono) sobre un bosque ⟹ `H¹ = 0`.
5//! 2. Añadir una arista: `H¹` no decrece y `H⁰` no crece.
6//! 3. El haz constante reproduce los números de Betti del grafo.
7//!
8//! La invariante 1 se acota a **bosques** a propósito: sobre grafos cíclicos la
9//! codificación lineal ve la obstrucción topológica aunque el dato sea monótono
10//! (§11 R1) — esa discrepancia está documentada, no es un bug.
11
12use proptest::prelude::*;
13use sheafsync::cohomology::compute_with;
14use sheafsync::gf2::Gf2Backend;
15use sheafsync::oracle::{Config, OracleVerdict, Share};
16use sheafsync::sheaf::Sheaf;
17
18/// `(dim H⁰, dim H¹)` del haz constante `d=1` sobre `(n, edges)`.
19fn coho(n: usize, edges: &[(usize, usize)]) -> (usize, usize) {
20    let sheaf = Sheaf::constant(n, edges, 1);
21    let c = compute_with(&sheaf, &Gf2Backend).unwrap();
22    (c.dim_h0, c.dim_h1)
23}
24
25/// Número de componentes conexas por union-find.
26fn componentes(n: usize, edges: &[(usize, usize)]) -> usize {
27    let mut parent: Vec<usize> = (0..n).collect();
28    fn find(parent: &mut [usize], x: usize) -> usize {
29        let mut r = x;
30        while parent[r] != r {
31            r = parent[r];
32        }
33        // compresión de caminos
34        let mut c = x;
35        while parent[c] != c {
36            let next = parent[c];
37            parent[c] = r;
38            c = next;
39        }
40        r
41    }
42    for &(a, b) in edges {
43        let ra = find(&mut parent, a);
44        let rb = find(&mut parent, b);
45        if ra != rb {
46            parent[ra] = rb;
47        }
48    }
49    (0..n).filter(|&x| find(&mut parent, x) == x).count()
50}
51
52/// Grafo aleatorio: `n` vértices y una lista de aristas (posibles multiaristas).
53fn grafo() -> impl Strategy<Value = (usize, Vec<(usize, usize)>)> {
54    (2usize..=6).prop_flat_map(|n| {
55        let arista = (0..n, 0..n).prop_filter("sin lazos", |(a, b)| a != b);
56        (Just(n), prop::collection::vec(arista, 0..10))
57    })
58}
59
60/// Grafo aleatorio más una arista extra dentro del mismo rango de vértices.
61fn grafo_y_arista() -> impl Strategy<Value = (usize, Vec<(usize, usize)>, (usize, usize))> {
62    (2usize..=6).prop_flat_map(|n| {
63        let arista = (0..n, 0..n).prop_filter("sin lazos", |(a, b)| a != b);
64        (Just(n), prop::collection::vec(arista.clone(), 0..10), arista)
65    })
66}
67
68proptest! {
69    /// Invariante 3: haz constante ⟹ `H⁰ = #componentes`, `H¹ = E − V + C`.
70    #[test]
71    fn haz_constante_reproduce_betti((n, edges) in grafo()) {
72        let (h0, h1) = coho(n, &edges);
73        let c = componentes(n, &edges);
74        let e = edges.len();
75        prop_assert_eq!(h0, c, "H⁰ debe contar componentes");
76        // E − V + C ≥ 0 siempre; lo calculamos sin subdesbordar.
77        prop_assert_eq!(h1 + n, e + c, "H¹ debe ser el primer número de Betti");
78    }
79
80    /// Invariante 2: añadir una arista no reduce `H¹` ni aumenta `H⁰`.
81    #[test]
82    fn anadir_arista_no_reduce_h1_ni_aumenta_h0((n, edges, extra) in grafo_y_arista()) {
83        let (h0, h1) = coho(n, &edges);
84        let mut mas = edges.clone();
85        mas.push(extra);
86        let (h0b, h1b) = coho(n, &mas);
87        prop_assert!(h1b >= h1, "H¹ no debe decrecer al añadir una arista");
88        prop_assert!(h0b <= h0, "H⁰ no debe crecer al añadir una arista");
89    }
90
91    /// Invariante nuevo de la pista de retículos (Addendum §F.3), el que el MVP
92    /// lineal NO podía satisfacer: **monótono sobre grafo arbitrario (cíclico
93    /// incluido) ⟹ corre libre** por la ruta de Tarski.
94    #[test]
95    fn monotono_sobre_grafo_arbitrario_corre_libre_via_tarski((n, edges) in grafo()) {
96        let shares = edges.iter().map(|&(a, b)| Share::monotona(a, b)).collect();
97        let config = Config::new("mono-arbitrario", n, shares);
98        prop_assert_eq!(config.oracle_verdict(), OracleVerdict::CoordinationFree);
99        prop_assert_eq!(config.tarski_verdict(), OracleVerdict::CoordinationFree);
100    }
101
102    /// Invariante 1 (MVP lineal): solo-suma sobre un bosque ⟹ `H¹ = 0` y el
103    /// oráculo y el haz lineal coinciden en "corre libre".
104    #[test]
105    fn monotono_sobre_bosque_corre_libre((n, edges) in grafo()) {
106        // Quedarnos solo con las aristas que conectan componentes nuevas → bosque.
107        let mut parent: Vec<usize> = (0..n).collect();
108        fn find(parent: &mut [usize], x: usize) -> usize {
109            let mut r = x;
110            while parent[r] != r { r = parent[r]; }
111            r
112        }
113        let mut bosque = Vec::new();
114        for (a, b) in edges {
115            let ra = find(&mut parent, a);
116            let rb = find(&mut parent, b);
117            if ra != rb {
118                parent[ra] = rb;
119                bosque.push(Share::monotona(a, b));
120            }
121        }
122        let config = Config::new("bosque-aleatorio", n, bosque);
123        prop_assert_eq!(config.oracle_verdict(), OracleVerdict::CoordinationFree);
124        prop_assert_eq!(config.sheaf_verdict(), OracleVerdict::CoordinationFree);
125    }
126}