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 1: solo-suma (monótono) sobre un bosque ⟹ `H¹ = 0` y el
92    /// oráculo y el haz coinciden en "corre libre".
93    #[test]
94    fn monotono_sobre_bosque_corre_libre((n, edges) in grafo()) {
95        // Quedarnos solo con las aristas que conectan componentes nuevas → bosque.
96        let mut parent: Vec<usize> = (0..n).collect();
97        fn find(parent: &mut [usize], x: usize) -> usize {
98            let mut r = x;
99            while parent[r] != r { r = parent[r]; }
100            r
101        }
102        let mut bosque = Vec::new();
103        for (a, b) in edges {
104            let ra = find(&mut parent, a);
105            let rb = find(&mut parent, b);
106            if ra != rb {
107                parent[ra] = rb;
108                bosque.push(Share::monotona(a, b));
109            }
110        }
111        let config = Config::new("bosque-aleatorio", n, bosque);
112        prop_assert_eq!(config.oracle_verdict(), OracleVerdict::CoordinationFree);
113        prop_assert_eq!(config.sheaf_verdict(), OracleVerdict::CoordinationFree);
114    }
115}