minerva 0.2.0

use super::*;
use proptest::prelude::*;

/// A literal identity for the fixtures below (test machinery).
fn d(station: u32, counter: u64) -> Dot {
    Dot::from_parts(station, counter).expect("a test dot has a nonzero counter")
}

/// The S200 region plane, one link-cut node per placed dot: the
/// contract form the segmented plane must agree with on every read,
/// kept verbatim as the dual-form oracle.
#[derive(Clone, Debug)]
struct NaiveRegions {
    starts: EndpointForest,
    ends: EndpointForest,
    dots: Vec<Dot>,
    index: BTreeMap<Dot, u32>,
}

impl NaiveRegions {
    fn new() -> Self {
        Self {
            starts: EndpointForest { nodes: Vec::new() },
            ends: EndpointForest { nodes: Vec::new() },
            dots: Vec::new(),
            index: BTreeMap::new(),
        }
    }

    fn insert(&mut self, dot: Dot) -> bool {
        if self.index.contains_key(&dot) {
            return false;
        }
        let id = u32::try_from(self.dots.len()).expect("test scale fits");
        self.starts.push_node();
        self.ends.push_node();
        self.dots.push(dot);
        let _ = self.index.insert(dot, id);
        true
    }

    fn remove(&mut self, dot: Dot) -> bool {
        let Some(id) = self.index.remove(&dot) else {
            return false;
        };
        self.starts.reset(id);
        self.ends.reset(id);
        true
    }

    fn endpoint(&mut self, dot: Dot, boundary: RegionBoundary) -> Option<Dot> {
        let id = *self.index.get(&dot)?;
        let root = match boundary {
            RegionBoundary::Start => self.starts.root(id),
            RegionBoundary::End => self.ends.root(id),
        };
        Some(self.dots[root as usize])
    }

    fn replace(&mut self, dot: Dot, child: Option<Dot>, boundary: RegionBoundary) -> bool {
        let Some(&id) = self.index.get(&dot) else {
            return false;
        };
        let child = match child {
            Some(child) => {
                let Some(&child) = self.index.get(&child) else {
                    return false;
                };
                Some(child)
            }
            None => None,
        };
        match boundary {
            RegionBoundary::Start => self.starts.replace_parent(id, child),
            RegionBoundary::End => self.ends.replace_parent(id, child),
        }
        true
    }
}

/// One step of the region planes' life, mirroring the production
/// protocol: placements, last-child edge replacements on both sides
/// (successor-shaped and explicit alike), edge cuts, and the
/// replace-then-retire excision order.
#[derive(Clone, Debug)]
enum RegionOp {
    Insert { station: u8, index: u8 },
    ReplaceEnd { station: u8, index: u8, child: u8 },
    ReplaceStart { station: u8, index: u8, child: u8 },
    Cut { station: u8, index: u8 },
    Remove { station: u8, index: u8 },
}

fn arb_region_op() -> impl Strategy<Value = RegionOp> {
    prop_oneof![
        4 => (0..2u8, 1..24u8)
            .prop_map(|(station, index)| RegionOp::Insert { station, index }),
        4 => (0..2u8, 1..24u8, 1..24u8)
            .prop_map(|(station, index, child)| RegionOp::ReplaceEnd { station, index, child }),
        2 => (0..2u8, 1..24u8, 1..24u8).prop_map(|(station, index, child)| {
            RegionOp::ReplaceStart { station, index, child }
        }),
        1 => (0..2u8, 1..24u8).prop_map(|(station, index)| RegionOp::Cut { station, index }),
        1 => (0..2u8, 1..24u8).prop_map(|(station, index)| RegionOp::Remove { station, index }),
    ]
}

/// The anchor-forest model the tapes respect: `ends_child[x] = y`
/// means y is x's last After child, and a dot has one parent per
/// side (the production protocol's own shape, which is what keeps
/// both planes' acyclicity preconditions honest).
#[derive(Default)]
struct EdgeModel {
    ends_child: BTreeMap<Dot, Dot>,
    ends_parent: BTreeMap<Dot, Dot>,
    starts_child: BTreeMap<Dot, Dot>,
    starts_parent: BTreeMap<Dot, Dot>,
    placed: BTreeSet<Dot>,
}

impl EdgeModel {
    fn cycle_through(&self, from: Dot, target: Dot, ends: bool) -> bool {
        let map = if ends {
            &self.ends_child
        } else {
            &self.starts_child
        };
        let mut cursor = Some(from);
        while let Some(dot) = cursor {
            if dot == target {
                return true;
            }
            cursor = map.get(&dot).copied();
        }
        false
    }

    fn set_edge(&mut self, dot: Dot, child: Option<Dot>, ends: bool) -> bool {
        if !self.placed.contains(&dot) {
            return false;
        }
        if let Some(child) = child {
            if !self.placed.contains(&child) {
                return false;
            }
            // The one-parent-per-side and acyclicity preconditions the
            // production anchor forest guarantees structurally.
            let parent_map = if ends {
                &self.ends_parent
            } else {
                &self.starts_parent
            };
            if parent_map.get(&child).is_some_and(|&p| p != dot) {
                return false;
            }
            if self.cycle_through(child, dot, ends) {
                return false;
            }
        }
        let (child_map, parent_map) = if ends {
            (&mut self.ends_child, &mut self.ends_parent)
        } else {
            (&mut self.starts_child, &mut self.starts_parent)
        };
        if let Some(old) = child_map.remove(&dot) {
            let _ = parent_map.remove(&old);
        }
        if let Some(child) = child {
            let _ = child_map.insert(dot, child);
            let _ = parent_map.insert(child, dot);
        }
        true
    }
}

proptest! {
    /// The dual-form agreement pin (the shell discipline's one law,
    /// applied to the region planes): over any edge tape the
    /// production protocol could issue, the segmented plane and the
    /// S200 per-dot plane agree on every verdict and every endpoint
    /// read, on both sides, for every placed dot.
    #[test]
    fn prop_segment_plane_agrees_with_the_per_dot_form(
        ops in prop::collection::vec(arb_region_op(), 0..80),
    ) {
        let mut segmented = RegionEnds::new();
        let mut naive = NaiveRegions::new();
        let mut model = EdgeModel::default();
        for op in &ops {
            match *op {
                RegionOp::Insert { station, index } => {
                    let dot = d(u32::from(station), u64::from(index));
                    let fresh = model.placed.insert(dot);
                    prop_assert_eq!(segmented.insert(dot), fresh);
                    prop_assert_eq!(naive.insert(dot), fresh);
                }
                RegionOp::ReplaceEnd { station, index, child } => {
                    let dot = d(u32::from(station), u64::from(index));
                    let child = d(u32::from(station), u64::from(child));
                    if model.set_edge(dot, Some(child), true) {
                        prop_assert!(segmented.replace(dot, Some(child), RegionBoundary::End));
                        prop_assert!(naive.replace(dot, Some(child), RegionBoundary::End));
                    }
                }
                RegionOp::ReplaceStart { station, index, child } => {
                    let dot = d(u32::from(station), u64::from(index));
                    let child = d(u32::from(station), u64::from(child));
                    if child != dot && model.set_edge(dot, Some(child), false) {
                        prop_assert!(
                            segmented.replace(dot, Some(child), RegionBoundary::Start)
                        );
                        prop_assert!(naive.replace(dot, Some(child), RegionBoundary::Start));
                    }
                }
                RegionOp::Cut { station, index } => {
                    let dot = d(u32::from(station), u64::from(index));
                    if model.set_edge(dot, None, true) {
                        prop_assert!(segmented.replace(dot, None, RegionBoundary::End));
                        prop_assert!(naive.replace(dot, None, RegionBoundary::End));
                    }
                }
                RegionOp::Remove { station, index } => {
                    let dot = d(u32::from(station), u64::from(index));
                    if model.placed.contains(&dot) {
                        // The excision protocol, in condense's own order:
                        // the parent's edge to the dot is replaced away
                        // first, then the dot's own edges, then the
                        // retirement.
                        let ends_parent = model.ends_parent.get(&dot).copied();
                        let starts_parent = model.starts_parent.get(&dot).copied();
                        if let Some(parent) = ends_parent {
                            prop_assert!(model.set_edge(parent, None, true));
                            prop_assert!(
                                segmented.replace(parent, None, RegionBoundary::End)
                            );
                            prop_assert!(naive.replace(parent, None, RegionBoundary::End));
                        }
                        if let Some(parent) = starts_parent {
                            prop_assert!(model.set_edge(parent, None, false));
                            prop_assert!(
                                segmented.replace(parent, None, RegionBoundary::Start)
                            );
                            prop_assert!(naive.replace(parent, None, RegionBoundary::Start));
                        }
                        let _ = model.set_edge(dot, None, true);
                        let _ = model.set_edge(dot, None, false);
                        let _ = segmented.replace(dot, None, RegionBoundary::End);
                        let _ = segmented.replace(dot, None, RegionBoundary::Start);
                        let _ = naive.replace(dot, None, RegionBoundary::End);
                        let _ = naive.replace(dot, None, RegionBoundary::Start);
                        let _ = model.placed.remove(&dot);
                        prop_assert!(segmented.remove(dot));
                        prop_assert!(naive.remove(dot));
                    }
                }
            }
            for &dot in &model.placed {
                for boundary in [RegionBoundary::Start, RegionBoundary::End] {
                    prop_assert_eq!(
                        segmented.endpoint(dot, boundary),
                        naive.endpoint(dot, boundary),
                        "endpoints disagree at {:?} {:?}",
                        dot,
                        boundary
                    );
                }
            }
            segmented.check_invariants();
        }
    }
}

#[test]
fn a_typed_chain_allocates_no_forest_node() {
    // The hot path's whole point: appending at the tail is set
    // arithmetic, never allocation or a link-cut operation, and the
    // chain stays one segment.
    let mut regions = RegionEnds::new();
    assert!(regions.insert(d(1, 1)));
    for index in 2..=200u64 {
        assert!(regions.insert(d(1, index)));
        assert!(regions.replace(d(1, index - 1), Some(d(1, index)), RegionBoundary::End));
    }
    assert_eq!(regions.ends.segments(), 1, "a typed chain is one segment");
    assert_eq!(
        regions.ends.live_nodes(),
        0,
        "no edge ever touched the forest"
    );
    assert_eq!(regions.starts.live_nodes(), 0);
    for index in 1..=200u64 {
        assert_eq!(
            regions.endpoint(d(1, index), RegionBoundary::End),
            Some(d(1, 200))
        );
        assert_eq!(
            regions.endpoint(d(1, index), RegionBoundary::Start),
            Some(d(1, index)),
            "chain interiors have no Before children"
        );
    }
    regions.check_invariants();
}

#[test]
fn a_mid_chain_split_inherits_the_stored_edge() {
    // A segment with a stored tail edge splits mid-chain: the lower
    // half keeps the head identity and gains the fresh edge, the
    // upper half inherits the stored one, and every endpoint stays
    // exact (the edge-inheritance arm the naive form never needed).
    let mut regions = RegionEnds::new();
    for index in 1..=8u64 {
        assert!(regions.insert(d(1, index)));
        if index > 1 {
            assert!(regions.replace(d(1, index - 1), Some(d(1, index)), RegionBoundary::End));
        }
    }
    assert!(regions.insert(d(2, 1)));
    // The chain's tail edge: (1,8)'s last child is a foreign dot.
    assert!(regions.replace(d(1, 8), Some(d(2, 1)), RegionBoundary::End));
    assert_eq!(
        regions.endpoint(d(1, 3), RegionBoundary::End),
        Some(d(2, 1))
    );
    // A concurrent sibling outranks the successor mid-chain: (1,4)'s
    // last child stops being (1,5).
    assert!(regions.insert(d(2, 2)));
    assert!(regions.replace(d(1, 4), Some(d(2, 2)), RegionBoundary::End));
    assert_eq!(
        regions.endpoint(d(1, 3), RegionBoundary::End),
        Some(d(2, 2)),
        "the lower half follows the fresh edge"
    );
    assert_eq!(
        regions.endpoint(d(1, 5), RegionBoundary::End),
        Some(d(2, 1)),
        "the upper half inherited the stored edge"
    );
    assert_eq!(regions.ends.segments(), 4);
    regions.check_invariants();
}

#[test]
fn a_ceiling_dot_replaces_without_overflow() {
    // The successor probe at the dot ceiling refuses instead of
    // overflowing (the S200/S201 checked_add discipline).
    let mut regions = RegionEnds::new();
    assert!(regions.insert(d(1, u64::MAX)));
    assert!(regions.insert(d(2, 1)));
    assert!(regions.replace(d(1, u64::MAX), Some(d(2, 1)), RegionBoundary::End));
    assert_eq!(
        regions.endpoint(d(1, u64::MAX), RegionBoundary::End),
        Some(d(2, 1))
    );
    assert!(regions.replace(d(1, u64::MAX), None, RegionBoundary::End));
    assert_eq!(
        regions.endpoint(d(1, u64::MAX), RegionBoundary::End),
        Some(d(1, u64::MAX))
    );
    regions.check_invariants();
}

#[test]
fn region_end_replacement_does_not_capture_the_old_sibling() {
    let mut regions = RegionEnds::new();
    for index in 1..=5u64 {
        assert!(regions.insert(d(1, index)));
    }
    assert!(regions.replace(d(1, 1), Some(d(1, 2)), RegionBoundary::End));
    assert!(regions.replace(d(1, 2), Some(d(1, 3)), RegionBoundary::End));
    assert_eq!(
        regions.endpoint(d(1, 1), RegionBoundary::End),
        Some(d(1, 3))
    );
    assert_eq!(
        regions.endpoint(d(1, 2), RegionBoundary::End),
        Some(d(1, 3))
    );

    // A new last sibling changes the parent's region, not the old
    // sibling's region. This is the distinction a union-find cannot
    // represent.
    assert!(regions.replace(d(1, 1), Some(d(1, 4)), RegionBoundary::End));
    assert_eq!(
        regions.endpoint(d(1, 1), RegionBoundary::End),
        Some(d(1, 4))
    );
    assert_eq!(
        regions.endpoint(d(1, 2), RegionBoundary::End),
        Some(d(1, 3))
    );

    assert!(regions.replace(d(1, 4), Some(d(1, 5)), RegionBoundary::End));
    assert_eq!(
        regions.endpoint(d(1, 1), RegionBoundary::End),
        Some(d(1, 5))
    );
    assert!(regions.replace(d(1, 1), None, RegionBoundary::End));
    assert_eq!(
        regions.endpoint(d(1, 1), RegionBoundary::End),
        Some(d(1, 1))
    );
    assert_eq!(
        regions.endpoint(d(1, 4), RegionBoundary::End),
        Some(d(1, 5))
    );
    regions.check_invariants();
}