//! Property-based distribution tests — invariants that must hold across configs.
//!
//! Each test verifies a structural property across multiple simulation
//! configurations with varying fault conditions.

use simulation::distribution::properties::{
    check_cache_bounded, check_registry_propagation, check_repair_queue_populated,
    check_routing_table_bounded,
};
use simulation::distribution::sim::{
    run_simulation_with_nodes, DistributionSimConfig, SimAction,
};

// ────────────────────────────────────────────────────────────────────────────
// 1. Routing table size ≤ alive membership at every round
// ────────────────────────────────────────────────────────────────────────────

#[test]
fn routing_table_bounded_across_configs() {
    let configs = vec![
        // Healthy 5-node cluster
        DistributionSimConfig {
            name: "rt-bound-healthy-5".into(),
            num_nodes: 5,
            num_rounds: 50,
            ticks_per_round: 3,
            ..DistributionSimConfig::default()
        },
        // 10-node cluster with 2 deaths
        DistributionSimConfig {
            name: "rt-bound-deaths-10".into(),
            num_nodes: 10,
            num_rounds: 60,
            ticks_per_round: 3,
            kill_schedule: vec![(15, 3), (25, 7)],
            ..DistributionSimConfig::default()
        },
        // 15-node cluster with 1 death
        DistributionSimConfig {
            name: "rt-bound-large-15".into(),
            num_nodes: 15,
            num_rounds: 60,
            ticks_per_round: 3,
            kill_schedule: vec![(20, 0)],
            ..DistributionSimConfig::default()
        },
    ];

    for config in configs {
        let name = config.name.clone();
        let (trace, _) = run_simulation_with_nodes(config);
        let result = check_routing_table_bounded(&trace);
        assert!(
            result.passed,
            "[{name}] routing table bounded invariant violated: {}",
            result.actual
        );
    }
}

// ────────────────────────────────────────────────────────────────────────────
// 2. Cache size ≤ cache_capacity at every round
// ────────────────────────────────────────────────────────────────────────────

#[test]
fn cache_bounded_across_configs() {
    let capacity = 100;
    let configs = vec![
        DistributionSimConfig {
            name: "cache-bound-5".into(),
            num_nodes: 5,
            num_rounds: 50,
            ticks_per_round: 3,
            actors_per_node: 5,
            cache_capacity: capacity,
            ..DistributionSimConfig::default()
        },
        DistributionSimConfig {
            name: "cache-bound-10-deaths".into(),
            num_nodes: 10,
            num_rounds: 60,
            ticks_per_round: 3,
            actors_per_node: 3,
            cache_capacity: capacity,
            kill_schedule: vec![(15, 2), (20, 5)],
            ..DistributionSimConfig::default()
        },
    ];

    for config in configs {
        let name = config.name.clone();
        let (trace, _) = run_simulation_with_nodes(config);
        let result = check_cache_bounded(&trace, capacity);
        assert!(
            result.passed,
            "[{name}] cache bounded invariant violated: {}",
            result.actual
        );
    }
}

// ────────────────────────────────────────────────────────────────────────────
// 3. Repair queue populates when node with directory entries dies
// ────────────────────────────────────────────────────────────────────────────

#[test]
fn repair_queue_populates_on_death_with_directory_entries() {
    // Node 2 has 3 actors. When it dies, repair queue should grow.
    let config = DistributionSimConfig {
        name: "repair-proportional".into(),
        num_nodes: 5,
        num_rounds: 80,
        ticks_per_round: 3,
        actors_per_node: 3,
        kill_schedule: vec![(15, 2)],
        ..DistributionSimConfig::default()
    };

    let (trace, _) = run_simulation_with_nodes(config);

    // Repair queue should be populated within 2-3 rounds of death detection
    let result = check_repair_queue_populated(&trace, 15);
    assert!(
        result.passed,
        "repair queue should fill after node with actors dies: {}",
        result.actual
    );

    // Check that the total repair queue size across survivors is proportional
    // to the dead node's directory entries (3 actors)
    let post_death_sizes: Vec<usize> = trace
        .snapshots_per_round
        .iter()
        .skip(20)
        .take(30)
        .flat_map(|round_snaps| {
            round_snaps
                .iter()
                .filter(|(_, s)| s.is_alive)
                .map(|(_, s)| s.repair_queue_size)
        })
        .collect();

    let max_repair = post_death_sizes.iter().max().copied().unwrap_or(0);
    assert!(
        max_repair >= 1,
        "at least one repair queue entry expected for dead node's actors, max seen: {max_repair}"
    );
}

// ────────────────────────────────────────────────────────────────────────────
// 4. Registry convergence — eventual consistency across configs
// ────────────────────────────────────────────────────────────────────────────

#[test]
fn registry_eventually_consistent_across_configs() {
    let configs = vec![
        // 5 nodes, 1 name
        (
            DistributionSimConfig {
                name: "reg-ec-simple".into(),
                num_nodes: 5,
                num_rounds: 50,
                ticks_per_round: 3,
                actors_per_node: 0,
                action_schedule: vec![
                    (5, SimAction::RegisterName { node_idx: 0, name: "svc-a".into() }),
                ],
                ..DistributionSimConfig::default()
            },
            1, // expected min registry size
        ),
        // 8 nodes, 3 names from different nodes
        (
            DistributionSimConfig {
                name: "reg-ec-multi".into(),
                num_nodes: 8,
                num_rounds: 60,
                ticks_per_round: 3,
                actors_per_node: 0,
                action_schedule: vec![
                    (5, SimAction::RegisterName { node_idx: 0, name: "alpha".into() }),
                    (5, SimAction::RegisterName { node_idx: 3, name: "beta".into() }),
                    (5, SimAction::RegisterName { node_idx: 6, name: "gamma".into() }),
                ],
                ..DistributionSimConfig::default()
            },
            3,
        ),
        // 5 nodes, register + kill owner, verify tombstone propagates
        (
            DistributionSimConfig {
                name: "reg-ec-death".into(),
                num_nodes: 5,
                num_rounds: 80,
                ticks_per_round: 3,
                actors_per_node: 0,
                action_schedule: vec![
                    (5, SimAction::RegisterName { node_idx: 0, name: "ephemeral".into() }),
                ],
                kill_schedule: vec![(15, 0)],
                ..DistributionSimConfig::default()
            },
            1, // tombstoned entry still counts as registry_size
        ),
    ];

    for (config, min_size) in configs {
        let name = config.name.clone();
        let (trace, _) = run_simulation_with_nodes(config);
        let result = check_registry_propagation(&trace, min_size);
        assert!(
            result.passed,
            "[{name}] registry should converge: {}",
            result.actual
        );
    }
}

// ────────────────────────────────────────────────────────────────────────────
// 5. Multiple deaths don't violate invariants
// ────────────────────────────────────────────────────────────────────────────

#[test]
fn cascading_deaths_maintain_invariants() {
    // 8 nodes, 3 die in sequence
    let config = DistributionSimConfig {
        name: "cascade-invariants".into(),
        num_nodes: 8,
        num_rounds: 100,
        ticks_per_round: 3,
        actors_per_node: 2,
        cache_capacity: 200,
        kill_schedule: vec![(10, 1), (20, 3), (30, 5)],
        ..DistributionSimConfig::default()
    };

    let (trace, _) = run_simulation_with_nodes(config);

    let rt_result = check_routing_table_bounded(&trace);
    assert!(
        rt_result.passed,
        "routing table bounded after cascading deaths: {}",
        rt_result.actual
    );

    let cache_result = check_cache_bounded(&trace, 200);
    assert!(
        cache_result.passed,
        "cache bounded after cascading deaths: {}",
        cache_result.actual
    );

    let repair_result = check_repair_queue_populated(&trace, 10);
    assert!(
        repair_result.passed,
        "repair queue populated after first death: {}",
        repair_result.actual
    );
}