//! Invariantes basadas en propiedades (§9), que `proptest` intenta romper.
//!
//! Tres invariantes:
//! 1. Solo-suma (monótono) sobre un bosque ⟹ `H¹ = 0`.
//! 2. Añadir una arista: `H¹` no decrece y `H⁰` no crece.
//! 3. El haz constante reproduce los números de Betti del grafo.
//!
//! La invariante 1 se acota a **bosques** a propósito: sobre grafos cíclicos la
//! codificación lineal ve la obstrucción topológica aunque el dato sea monótono
//! (§11 R1) — esa discrepancia está documentada, no es un bug.

use proptest::prelude::*;
use sheafsync::cohomology::compute_with;
use sheafsync::gf2::Gf2Backend;
use sheafsync::oracle::{Config, OracleVerdict, Share};
use sheafsync::sheaf::Sheaf;

/// `(dim H⁰, dim H¹)` del haz constante `d=1` sobre `(n, edges)`.
fn coho(n: usize, edges: &[(usize, usize)]) -> (usize, usize) {
    let sheaf = Sheaf::constant(n, edges, 1);
    let c = compute_with(&sheaf, &Gf2Backend).unwrap();
    (c.dim_h0, c.dim_h1)
}

/// Número de componentes conexas por union-find.
fn componentes(n: usize, edges: &[(usize, usize)]) -> usize {
    let mut parent: Vec<usize> = (0..n).collect();
    fn find(parent: &mut [usize], x: usize) -> usize {
        let mut r = x;
        while parent[r] != r {
            r = parent[r];
        }
        // compresión de caminos
        let mut c = x;
        while parent[c] != c {
            let next = parent[c];
            parent[c] = r;
            c = next;
        }
        r
    }
    for &(a, b) in edges {
        let ra = find(&mut parent, a);
        let rb = find(&mut parent, b);
        if ra != rb {
            parent[ra] = rb;
        }
    }
    (0..n).filter(|&x| find(&mut parent, x) == x).count()
}

/// Grafo aleatorio: `n` vértices y una lista de aristas (posibles multiaristas).
fn grafo() -> impl Strategy<Value = (usize, Vec<(usize, usize)>)> {
    (2usize..=6).prop_flat_map(|n| {
        let arista = (0..n, 0..n).prop_filter("sin lazos", |(a, b)| a != b);
        (Just(n), prop::collection::vec(arista, 0..10))
    })
}

/// Grafo aleatorio más una arista extra dentro del mismo rango de vértices.
fn grafo_y_arista() -> impl Strategy<Value = (usize, Vec<(usize, usize)>, (usize, usize))> {
    (2usize..=6).prop_flat_map(|n| {
        let arista = (0..n, 0..n).prop_filter("sin lazos", |(a, b)| a != b);
        (Just(n), prop::collection::vec(arista.clone(), 0..10), arista)
    })
}

proptest! {
    /// Invariante 3: haz constante ⟹ `H⁰ = #componentes`, `H¹ = E − V + C`.
    #[test]
    fn haz_constante_reproduce_betti((n, edges) in grafo()) {
        let (h0, h1) = coho(n, &edges);
        let c = componentes(n, &edges);
        let e = edges.len();
        prop_assert_eq!(h0, c, "H⁰ debe contar componentes");
        // E − V + C ≥ 0 siempre; lo calculamos sin subdesbordar.
        prop_assert_eq!(h1 + n, e + c, "H¹ debe ser el primer número de Betti");
    }

    /// Invariante 2: añadir una arista no reduce `H¹` ni aumenta `H⁰`.
    #[test]
    fn anadir_arista_no_reduce_h1_ni_aumenta_h0((n, edges, extra) in grafo_y_arista()) {
        let (h0, h1) = coho(n, &edges);
        let mut mas = edges.clone();
        mas.push(extra);
        let (h0b, h1b) = coho(n, &mas);
        prop_assert!(h1b >= h1, "H¹ no debe decrecer al añadir una arista");
        prop_assert!(h0b <= h0, "H⁰ no debe crecer al añadir una arista");
    }

    /// Invariante 1: solo-suma (monótono) sobre un bosque ⟹ `H¹ = 0` y el
    /// oráculo y el haz coinciden en "corre libre".
    #[test]
    fn monotono_sobre_bosque_corre_libre((n, edges) in grafo()) {
        // Quedarnos solo con las aristas que conectan componentes nuevas → bosque.
        let mut parent: Vec<usize> = (0..n).collect();
        fn find(parent: &mut [usize], x: usize) -> usize {
            let mut r = x;
            while parent[r] != r { r = parent[r]; }
            r
        }
        let mut bosque = Vec::new();
        for (a, b) in edges {
            let ra = find(&mut parent, a);
            let rb = find(&mut parent, b);
            if ra != rb {
                parent[ra] = rb;
                bosque.push(Share::monotona(a, b));
            }
        }
        let config = Config::new("bosque-aleatorio", n, bosque);
        prop_assert_eq!(config.oracle_verdict(), OracleVerdict::CoordinationFree);
        prop_assert_eq!(config.sheaf_verdict(), OracleVerdict::CoordinationFree);
    }
}