//! Property tests for NavigationStack invariants (bd-3eis).
//!
//! Verifies that NavigationStack maintains its invariants under arbitrary
//! sequences of push/pop/forward/jump/reset operations, using deterministic
//! seeded random generation for reproducibility.
//!
//! All properties are tested across 10,000+ generated operation sequences.

use lore_tui::message::{EntityKey, Screen};
use lore_tui::navigation::NavigationStack;

// ---------------------------------------------------------------------------
// Seeded PRNG (xorshift64) — same as stress_tests.rs
// ---------------------------------------------------------------------------

struct Rng(u64);

impl Rng {
    fn new(seed: u64) -> Self {
        Self(seed.wrapping_add(1))
    }

    fn next(&mut self) -> u64 {
        let mut x = self.0;
        x ^= x << 13;
        x ^= x >> 7;
        x ^= x << 17;
        self.0 = x;
        x
    }

    fn range(&mut self, max: u64) -> u64 {
        self.next() % max
    }
}

// ---------------------------------------------------------------------------
// Random Screen and Operation generators
// ---------------------------------------------------------------------------

fn random_screen(rng: &mut Rng) -> Screen {
    match rng.range(12) {
        0 => Screen::Dashboard,
        1 => Screen::IssueList,
        2 => Screen::IssueDetail(EntityKey::issue(1, rng.range(100) as i64)),
        3 => Screen::MrList,
        4 => Screen::MrDetail(EntityKey::mr(1, rng.range(100) as i64)),
        5 => Screen::Search,
        6 => Screen::Timeline,
        7 => Screen::Who,
        8 => Screen::Trace,
        9 => Screen::FileHistory,
        10 => Screen::Sync,
        _ => Screen::Stats,
    }
}

#[derive(Debug)]
enum NavOp {
    Push(Screen),
    Pop,
    GoForward,
    JumpBack,
    JumpForward,
    ResetTo(Screen),
}

fn random_op(rng: &mut Rng) -> NavOp {
    match rng.range(10) {
        // Push is the most common operation.
        0..=4 => NavOp::Push(random_screen(rng)),
        5 | 6 => NavOp::Pop,
        7 => NavOp::GoForward,
        8 => NavOp::JumpBack,
        9 => NavOp::JumpForward,
        _ => NavOp::ResetTo(random_screen(rng)),
    }
}

fn apply_op(nav: &mut NavigationStack, op: &NavOp) {
    match op {
        NavOp::Push(screen) => {
            nav.push(screen.clone());
        }
        NavOp::Pop => {
            nav.pop();
        }
        NavOp::GoForward => {
            nav.go_forward();
        }
        NavOp::JumpBack => {
            nav.jump_back();
        }
        NavOp::JumpForward => {
            nav.jump_forward();
        }
        NavOp::ResetTo(screen) => {
            nav.reset_to(screen.clone());
        }
    }
}

// ---------------------------------------------------------------------------
// Properties
// ---------------------------------------------------------------------------

/// Property 1: Stack depth is always >= 1.
///
/// The NavigationStack always has at least one screen (the root).
/// No sequence of operations can empty it.
#[test]
fn prop_depth_always_at_least_one() {
    for seed in 0..1000 {
        let mut rng = Rng::new(seed);
        let mut nav = NavigationStack::new();

        for step in 0..100 {
            let op = random_op(&mut rng);
            apply_op(&mut nav, &op);

            assert!(
                nav.depth() >= 1,
                "depth < 1 at seed={seed}, step={step}, op={op:?}"
            );
        }
    }
}

/// Property 2: After push(X), current() == X.
///
/// Pushing a screen always makes it the current screen.
#[test]
fn prop_push_sets_current() {
    for seed in 0..1000 {
        let mut rng = Rng::new(seed);
        let mut nav = NavigationStack::new();

        for step in 0..100 {
            let screen = random_screen(&mut rng);
            nav.push(screen.clone());
            assert_eq!(
                nav.current(),
                &screen,
                "push didn't set current at seed={seed}, step={step}"
            );

            // Also do some random ops to make sequences varied.
            if rng.range(3) == 0 {
                let op = random_op(&mut rng);
                apply_op(&mut nav, &op);
            }
        }
    }
}

/// Property 3: After push(X) then pop(), current returns to previous.
///
/// Push-then-pop is identity on current() when no intermediate ops occur.
#[test]
fn prop_push_pop_returns_to_previous() {
    for seed in 0..1000 {
        let mut rng = Rng::new(seed);
        let mut nav = NavigationStack::new();

        // Do some random setup ops.
        for _ in 0..rng.range(20) {
            let op = random_op(&mut rng);
            apply_op(&mut nav, &op);
        }

        let before = nav.current().clone();
        let screen = random_screen(&mut rng);
        nav.push(screen);

        let pop_result = nav.pop();
        assert!(pop_result.is_some(), "pop after push should succeed");
        assert_eq!(
            nav.current(),
            &before,
            "push-pop should restore previous at seed={seed}"
        );
    }
}

/// Property 4: Forward stack is cleared after any push.
///
/// Browser semantics: navigating to a new page clears the forward history.
#[test]
fn prop_forward_cleared_after_push() {
    for seed in 0..1000 {
        let mut rng = Rng::new(seed);
        let mut nav = NavigationStack::new();

        // Build up some forward stack via push-pop sequences.
        for _ in 0..rng.range(10) + 2 {
            nav.push(random_screen(&mut rng));
        }
        for _ in 0..rng.range(5) + 1 {
            nav.pop();
        }
        // Now we might have forward entries.

        // Push clears forward.
        nav.push(random_screen(&mut rng));
        assert!(
            !nav.can_go_forward(),
            "forward stack should be empty after push at seed={seed}"
        );
    }
}

/// Property 5: Jump list only records detail/entity screens.
///
/// The jump list (vim Ctrl+O/Ctrl+I) only tracks IssueDetail and MrDetail.
/// After many operations, every jump_back/jump_forward target should be
/// a detail screen.
#[test]
fn prop_jump_list_only_details() {
    for seed in 0..500 {
        let mut rng = Rng::new(seed);
        let mut nav = NavigationStack::new();

        // Do many operations to build up jump list.
        for _ in 0..200 {
            let op = random_op(&mut rng);
            apply_op(&mut nav, &op);
        }

        // Walk the jump list backward and forward — every screen reached
        // should be a detail screen.
        let saved_current = nav.current().clone();

        let mut visited = Vec::new();
        while let Some(screen) = nav.jump_back() {
            visited.push(screen.clone());
        }
        while let Some(screen) = nav.jump_forward() {
            visited.push(screen.clone());
        }

        for screen in &visited {
            assert!(
                screen.is_detail_or_entity(),
                "jump list contained non-detail screen {screen:?} at seed={seed}"
            );
        }

        // Restore (this is a property test, not behavior test — we don't
        // care about restoring, just checking the invariant).
        let _ = saved_current;
    }
}

/// Property 6: reset_to(X) clears all history, current() == X.
///
/// After reset, depth == 1, no back, no forward, empty jump list.
#[test]
fn prop_reset_clears_all() {
    for seed in 0..1000 {
        let mut rng = Rng::new(seed);
        let mut nav = NavigationStack::new();

        // Build up complex state.
        for _ in 0..rng.range(50) + 10 {
            let op = random_op(&mut rng);
            apply_op(&mut nav, &op);
        }

        let target = random_screen(&mut rng);
        nav.reset_to(target.clone());

        assert_eq!(
            nav.current(),
            &target,
            "reset didn't set current at seed={seed}"
        );
        assert_eq!(
            nav.depth(),
            1,
            "reset didn't clear back stack at seed={seed}"
        );
        assert!(!nav.can_go_back(), "reset didn't clear back at seed={seed}");
        assert!(
            !nav.can_go_forward(),
            "reset didn't clear forward at seed={seed}"
        );
    }
}

/// Property 7: Breadcrumbs length == depth.
///
/// breadcrumbs() always returns exactly as many entries as the navigation
/// depth (back_stack + 1 for current).
#[test]
fn prop_breadcrumbs_match_depth() {
    for seed in 0..1000 {
        let mut rng = Rng::new(seed);
        let mut nav = NavigationStack::new();

        for step in 0..100 {
            let op = random_op(&mut rng);
            apply_op(&mut nav, &op);

            assert_eq!(
                nav.breadcrumbs().len(),
                nav.depth(),
                "breadcrumbs length != depth at seed={seed}, step={step}, op={op:?}"
            );
        }
    }
}

/// Property 8: No panic for any sequence of operations.
///
/// This is the "chaos monkey" property — the most important invariant.
#[test]
fn prop_no_panic_any_sequence() {
    for seed in 0..1000 {
        let mut rng = Rng::new(seed);
        let mut nav = NavigationStack::new();

        for _ in 0..200 {
            let op = random_op(&mut rng);
            apply_op(&mut nav, &op);
        }

        // If we got here, no panic occurred.
        assert!(nav.depth() >= 1);
    }
}

/// Property 9: Pop at root is always safe and returns None.
///
/// Repeated pops from any state eventually reach root and stop.
#[test]
fn prop_repeated_pop_reaches_root() {
    for seed in 0..1000 {
        let mut rng = Rng::new(seed);
        let mut nav = NavigationStack::new();

        // Push random depth.
        let pushes = rng.range(20) + 1;
        for _ in 0..pushes {
            nav.push(random_screen(&mut rng));
        }

        // Pop until we can't.
        let mut pops = 0;
        while nav.pop().is_some() {
            pops += 1;
            assert!(pops <= pushes, "more pops than pushes at seed={seed}");
        }

        assert_eq!(
            nav.depth(),
            1,
            "should be at root after exhaustive pop at seed={seed}"
        );
        // One more pop should be None.
        assert!(nav.pop().is_none());
    }
}

/// Property 10: Go forward after go back restores screen.
///
/// Pop-then-forward is identity (when no intermediate push).
#[test]
fn prop_pop_forward_identity() {
    for seed in 0..1000 {
        let mut rng = Rng::new(seed);
        let mut nav = NavigationStack::new();

        // Build some state.
        for _ in 0..rng.range(10) + 2 {
            nav.push(random_screen(&mut rng));
        }

        let before_pop = nav.current().clone();
        if nav.pop().is_some() {
            let result = nav.go_forward();
            assert!(
                result.is_some(),
                "forward should succeed after pop at seed={seed}"
            );
            assert_eq!(
                nav.current(),
                &before_pop,
                "pop-forward should restore screen at seed={seed}"
            );
        }
    }
}