aprender-core 0.31.2

// CONTRACT: pagerank-kernel-v1.yaml
// HASH: sha256:f6a7b8c9d0e12345
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`

use aprender::graph::{Graph, GraphCentrality};
use proptest::prelude::*;

proptest! {
    /// Obligation: Probability distribution (invariant)
    /// Formal: sum(r) ≈ 1, r_i >= 0
    #[test]
    fn prop_probability_distribution(
        n in 3usize..10
    ) {
        // Create a cycle graph: 0→1→2→...→(n-1)→0
        let edges: Vec<(usize, usize)> = (0..n).map(|i| (i, (i + 1) % n)).collect();
        let g = Graph::from_edges(&edges, true);
        let ranks = g.pagerank(0.85, 100, 1e-8).expect("pagerank succeeds");

        let sum: f64 = ranks.iter().sum();
        prop_assert!(
            (sum - 1.0).abs() < 1e-4,
            "sum(ranks)={sum}, expected ~1.0"
        );
    }

    /// Obligation: Scores non-negative (bound)
    /// Formal: r_i >= 0 for all i
    #[test]
    fn prop_scores_non_negative(
        n in 3usize..10
    ) {
        let edges: Vec<(usize, usize)> = (0..n).map(|i| (i, (i + 1) % n)).collect();
        let g = Graph::from_edges(&edges, true);
        let ranks = g.pagerank(0.85, 100, 1e-8).expect("pagerank succeeds");

        for (i, &r) in ranks.iter().enumerate() {
            prop_assert!(
                r >= 0.0,
                "rank[{i}]={r}, expected >= 0"
            );
        }
    }

    /// Obligation: Normalization preserved across iterations (invariant)
    /// Formal: sum(r) stays ≈ 1 across iterations
    #[test]
    fn prop_normalization_preserved(
        iters in 1usize..50
    ) {
        let g = Graph::from_edges(&[(0, 1), (1, 2), (2, 0), (0, 2)], true);
        let ranks = g.pagerank(0.85, iters, 1e-12).expect("pagerank succeeds");

        let sum: f64 = ranks.iter().sum();
        prop_assert!(
            (sum - 1.0).abs() < 0.01,
            "sum(ranks)={sum} after {iters} iterations, expected ~1.0"
        );
    }

    /// Obligation: Single node has rank 1.0 (boundary)
    /// Formal: single-node graph → rank = 1.0
    #[test]
    fn prop_single_node(_dummy in 0..1i32) {
        let g = Graph::from_edges(&[(0, 0)], true);
        let ranks = g.pagerank(0.85, 100, 1e-8).expect("pagerank succeeds");

        prop_assert_eq!(ranks.len(), 1);
        prop_assert!(
            (ranks[0] - 1.0).abs() < 1e-6,
            "single node rank={}, expected 1.0", ranks[0]
        );
    }

    /// Obligation: SIMD matches scalar within ULP (equivalence)
    #[test]
    #[ignore = "SIMD equivalence — trueno domain"]
    fn prop_simd_equivalence(
        _x in proptest::collection::vec(-10.0f32..10.0, 1..32usize)
    ) {
        // SIMD equivalence testing is trueno's responsibility
    }
}