minerva 0.2.0

extern crate std;

use super::super::placement::Locus;
use super::super::wire::apply_chain_step;
use super::*;
use crate::kairos::{Clock, Kairos, TickCounter};
use crate::metis::dot::RawDot;
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")
}

fn rank(salt: u16) -> Kairos {
    let clock = Clock::with_default_config(TickCounter::new(), 1).expect("test clock config");
    clock.now(salt)
}

/// The contract form, S116's grouping verbatim: every woven dot under
/// its anchor, buckets sorted in the sibling order. The oracle every
/// shell read is pinned against.
fn map_form(plane: &IdentityPlane) -> BTreeMap<Anchor, Vec<Dot>> {
    let mut children: BTreeMap<Anchor, Vec<Dot>> = BTreeMap::new();
    for (dot, locus) in plane.iter() {
        children.entry(locus.anchor).or_default().push(dot);
    }
    for bucket in children.values_mut() {
        bucket.sort_unstable_by(|a, b| sibling_cmp(plane, *a, *b));
    }
    children
}

/// Every read the consumers run, agreed against the contract form:
/// bucket contents in stored order, head, tail, point reads, the
/// climb's suffix and prefix slices, absent anchors answering nothing,
/// and the endpoint-registration enumeration.
fn assert_agrees(shell: &ChildPlane, plane: &IdentityPlane) {
    let oracle = map_form(plane);
    for (&anchor, expected) in &oracle {
        let bucket = shell
            .bucket(plane, anchor)
            .expect("a parent with children has a bucket");
        assert!(
            bucket.iter().eq(expected.iter().copied()),
            "bucket contents disagree at {anchor:?}"
        );
        assert_eq!(bucket.first(), expected[0]);
        assert_eq!(bucket.last(), *expected.last().expect("non-empty"));
        for (at, &dot) in expected.iter().enumerate() {
            assert_eq!(bucket.get(at), Some(dot));
            assert!(bucket.suffix(at).eq(expected[at + 1..].iter().copied()));
            assert!(
                bucket
                    .suffix(at)
                    .rev()
                    .eq(expected[at + 1..].iter().rev().copied())
            );
            assert!(bucket.prefix(at).eq(expected[..at].iter().copied()));
        }
        assert_eq!(bucket.get(expected.len()), None);
    }
    // No fabricated buckets: every anchor shape reachable from the woven
    // dots (plus the origin) that the oracle lacks answers nothing.
    let mut probes: Vec<Anchor> = alloc::vec![Anchor::Origin];
    for (dot, _) in plane.iter() {
        probes.push(Anchor::After(dot.into()));
        probes.push(Anchor::Before(dot.into()));
    }
    for anchor in probes {
        if !oracle.contains_key(&anchor) {
            assert!(
                shell.bucket(plane, anchor).is_none(),
                "a childless anchor grew a bucket at {anchor:?}"
            );
        }
    }
    // The endpoint-registration read: every parent paired with its last
    // child, exactly once each.
    let lasts: BTreeMap<Anchor, Dot> = shell.last_children(plane).collect();
    assert_eq!(
        lasts.len(),
        shell.last_children(plane).count(),
        "no anchor repeats"
    );
    let expected_lasts: BTreeMap<Anchor, Dot> = oracle
        .iter()
        .map(|(&anchor, bucket)| (anchor, *bucket.last().expect("non-empty")))
        .collect();
    assert_eq!(lasts, expected_lasts);
    // The from-parts build agrees with the incrementally maintained
    // shell on every read (spelling may differ; reads may not).
    let rebuilt = ChildPlane::build(plane);
    for (&anchor, expected) in &oracle {
        let bucket = rebuilt.bucket(plane, anchor).expect("rebuilt bucket");
        assert!(bucket.iter().eq(expected.iter().copied()));
    }
}

/// One step of the child plane's life, mirroring the production call
/// order exactly: a weave (plane insert then child insert), a chain
/// append (the coalesced spelling), or an excision (plane removal then
/// child removal). Anchors mix the origin, both sides of live dots,
/// dangling dots, and the self-anchor.
#[derive(Clone, Debug)]
enum Op {
    Weave {
        station: u32,
        index: u64,
        anchor_pick: u8,
        salt: u16,
    },
    Extend {
        station: u32,
        step: u64,
    },
    Remove {
        station: u32,
        index: u64,
    },
}

fn arb_op() -> impl Strategy<Value = Op> {
    prop_oneof![
        3 => (0..3u32, 1..=48u64, any::<u8>(), any::<u16>()).prop_map(
            |(station, index, anchor_pick, salt)| Op::Weave { station, index, anchor_pick, salt }
        ),
        3 => (0..3u32, prop_oneof![3 => Just(0u64), 1 => 1..=6u64])
            .prop_map(|(station, step)| Op::Extend { station, step }),
        2 => (0..3u32, 1..=48u64).prop_map(|(station, index)| Op::Remove { station, index }),
    ]
}

/// The anchor an op picks: the origin, either side of a woven dot (live
/// anchors, the common shape), a dangling dot, or the dot itself (the
/// self-anchor the wire tolerates).
fn pick_anchor(model: &BTreeMap<Dot, Locus>, dot: Dot, pick: u8) -> Anchor {
    let woven: Vec<Dot> = model.keys().copied().collect();
    match pick % 8 {
        0 => Anchor::Origin,
        1 => Anchor::After(dot.into()),
        2 => Anchor::Before(RawDot {
            station: dot.station(),
            counter: dot.counter().saturating_add(3),
        }),
        n if !woven.is_empty() => {
            let target: (u32, u64) = woven[usize::from(pick) % woven.len()].into();
            if n % 2 == 0 {
                Anchor::After(target.into())
            } else {
                Anchor::Before(target.into())
            }
        }
        _ => Anchor::Origin,
    }
}

proptest! {
    /// The dual-form agreement pin the shell discipline demands. Over
    /// any op tape run in the production call order, every read the
    /// consumers make of the coalesced child plane agrees with the
    /// S116 `BTreeMap<Anchor, Vec<Dot>>` contract form grouped and
    /// sorted fresh from the same skeleton, whatever spelling history
    /// (materialized residue, de-materialized survivors) the tape left
    /// behind.
    #[test]
    fn prop_child_plane_agrees_with_the_map_form(
        ops in prop::collection::vec(arb_op(), 0..60),
    ) {
        let mut plane = IdentityPlane::new();
        let mut shell = ChildPlane::new();
        let mut model: BTreeMap<Dot, Locus> = BTreeMap::new();
        let mut tails: BTreeMap<u32, u64> = BTreeMap::new();
        for op in &ops {
            match *op {
                Op::Weave { station, index, anchor_pick, salt } => {
                    let dot = d(station, index);
                    let anchor = pick_anchor(&model, dot, anchor_pick);
                    let value = Locus { anchor, rank: rank(salt) };
                    if plane.insert(dot, value) {
                        let _ = model.insert(dot, value);
                        shell.insert(&plane, anchor, dot);
                    }
                }
                Op::Extend { station, step } => {
                    let tail = tails.entry(station).or_insert(1);
                    let index = *tail;
                    let prev_dot = (station, index - 1);
                    let value = match Dot::try_from(prev_dot).ok().and_then(|p| model.get(&p)) {
                        Some(prev) if index > 1 => apply_chain_step(prev_dot, prev, step),
                        _ => Locus {
                            anchor: Anchor::Origin,
                            rank: Kairos::new(2_000 + index, 0, station.max(1), 3u16),
                        },
                    };
                    let dot = d(station, index);
                    if plane.insert(dot, value) {
                        let _ = model.insert(dot, value);
                        shell.insert(&plane, value.anchor, dot);
                    }
                    *tail += 1;
                }
                Op::Remove { station, index } => {
                    let dot = d(station, index);
                    if let Some(locus) = plane.get(&dot) {
                        // The endpoint-replacement read is the exact
                        // biconditional: `Replaced` fires iff the dot
                        // WAS the stored tail (and carries the new
                        // one); `Unchanged` means it was not, and the
                        // tail genuinely did not move.
                        let pre_tail = map_form(&plane)
                            .get(&locus.anchor)
                            .map(|bucket| *bucket.last().expect("non-empty"))
                            .expect("a woven dot is in its anchor's bucket");
                        let _ = plane.remove(dot).expect("probed present");
                        let _ = model.remove(&dot);
                        let post_tail = map_form(&plane).get(&locus.anchor).map(
                            |bucket| *bucket.last().expect("non-empty"),
                        );
                        match shell.remove(&plane, locus.anchor, dot) {
                            TailChange::Replaced(new_last) => {
                                prop_assert_eq!(dot, pre_tail);
                                prop_assert_eq!(new_last, post_tail);
                            }
                            TailChange::Unchanged => {
                                prop_assert_ne!(dot, pre_tail);
                                prop_assert_eq!(post_tail, Some(pre_tail));
                            }
                        }
                    }
                }
            }
            assert_agrees(&shell, &plane);
        }
    }
}

/// A chain of `len` elements: the head anchored at the origin, each
/// interior anchored after its predecessor with the clock-successor
/// rank, the shape the plane spells without this module storing a byte.
fn weave_chain(plane: &mut IdentityPlane, shell: &mut ChildPlane, station: u32, len: u64) {
    let head = Locus {
        anchor: Anchor::Origin,
        rank: Kairos::new(1_000, 5, station, 7u16),
    };
    assert!(plane.insert(d(station, 1), head));
    shell.insert(plane, Anchor::Origin, d(station, 1));
    let (mut prev_dot, mut prev) = ((station, 1), head);
    for index in 2..=len {
        let dot = d(station, index);
        let value = apply_chain_step(prev_dot, &prev, 0);
        assert!(plane.insert(dot, value));
        shell.insert(plane, value.anchor, dot);
        (prev_dot, prev) = (dot.into(), value);
    }
}

#[test]
fn a_chain_stores_no_explicit_bucket() {
    let mut plane = IdentityPlane::new();
    let mut shell = ChildPlane::new();
    weave_chain(&mut plane, &mut shell, 3, 200);
    assert_eq!(
        shell.explicit_buckets(),
        1,
        "only the origin bucket is stored"
    );
    assert_eq!(shell.explicit_children(), 1);
    for index in 1..200u64 {
        let bucket = shell
            .bucket(
                &plane,
                Anchor::After(RawDot {
                    station: 3,
                    counter: index,
                }),
            )
            .expect("a chain parent has its successor");
        assert!(matches!(bucket, Bucket::Implicit(_)));
        assert_eq!(bucket.first(), d(3, index + 1));
        assert_eq!(bucket.last(), d(3, index + 1));
    }
    assert!(
        shell
            .bucket(
                &plane,
                Anchor::After(RawDot {
                    station: 3,
                    counter: 200
                })
            )
            .is_none()
    );
    assert_agrees(&shell, &plane);
}

#[test]
fn a_second_sibling_materializes_and_departs() {
    let mut plane = IdentityPlane::new();
    let mut shell = ChildPlane::new();
    weave_chain(&mut plane, &mut shell, 1, 8);
    // A concurrent sibling lands beside the incumbent implicit child.
    let sibling = d(2, 1);
    let anchor = Anchor::After(RawDot {
        station: 1,
        counter: 4,
    });
    let value = Locus {
        anchor,
        rank: rank(9),
    };
    assert!(plane.insert(sibling, value));
    shell.insert(&plane, anchor, sibling);
    assert_eq!(
        shell.explicit_buckets(),
        2,
        "the contested bucket materialized"
    );
    let bucket = shell.bucket(&plane, anchor).expect("two children");
    assert_eq!(bucket.iter().count(), 2);
    assert_agrees(&shell, &plane);
    // The sibling's excision de-materializes: the survivor is the chain
    // child the plane spells alone.
    let removed = plane.remove(sibling).expect("the sibling was woven");
    let last_changed = shell.remove(&plane, removed.anchor, sibling);
    assert_eq!(shell.explicit_buckets(), 1, "the bucket de-materialized");
    // Whether the sibling was the stored tail depends on ranks; the
    // surviving read must be the implicit chain child either way.
    if let TailChange::Replaced(new_last) = last_changed {
        assert_eq!(new_last, Some(d(1, 5)));
    }
    let bucket = shell
        .bucket(&plane, anchor)
        .expect("the chain child remains");
    assert!(matches!(bucket, Bucket::Implicit(dot) if dot == d(1, 5)));
    assert_agrees(&shell, &plane);
}

#[test]
fn removing_a_non_tail_sibling_reports_unchanged() {
    // The reviewer's shape (the S201 gate review's observation): on a
    // multi-child bucket, removing a member that is NOT the stored
    // tail must report `Unchanged`, and removing the tail must report
    // the survivor, so a wrong verdict cannot hide behind "a child
    // remains".
    let mut plane = IdentityPlane::new();
    let mut shell = ChildPlane::new();
    weave_chain(&mut plane, &mut shell, 1, 4);
    let anchor = Anchor::After(RawDot {
        station: 1,
        counter: 2,
    });
    for (station, salt) in [(2u32, 9u16), (3, 11)] {
        let sibling = d(station, 1);
        let value = Locus {
            anchor,
            rank: rank(salt),
        };
        assert!(plane.insert(sibling, value));
        shell.insert(&plane, anchor, sibling);
    }
    let bucket: Vec<Dot> = shell
        .bucket(&plane, anchor)
        .expect("three children")
        .iter()
        .collect();
    assert_eq!(bucket.len(), 3);
    let (head, tail) = (bucket[0], bucket[2]);
    let removed = plane.remove(head).expect("the head was woven");
    assert_eq!(
        shell.remove(&plane, removed.anchor, head),
        TailChange::Unchanged,
        "removing a non-tail sibling moves no endpoint edge"
    );
    assert_eq!(
        shell.bucket(&plane, anchor).expect("two remain").last(),
        tail
    );
    let removed = plane.remove(tail).expect("the tail was woven");
    assert_eq!(
        shell.remove(&plane, removed.anchor, tail),
        TailChange::Replaced(Some(bucket[1])),
        "removing the tail replaces the endpoint edge with the survivor"
    );
    assert_agrees(&shell, &plane);
}

#[test]
fn a_ceiling_dot_probes_no_successor() {
    // The chain-child probe takes the successor through `checked_add`,
    // so the dot-space ceiling is a refusal, never an overflow (the
    // S200 coalescing-probe lesson, applied at design time).
    let mut plane = IdentityPlane::new();
    let mut shell = ChildPlane::new();
    let ceiling = d(5, u64::MAX);
    let head = Locus {
        anchor: Anchor::Origin,
        rank: rank(1),
    };
    assert!(plane.insert(ceiling, head));
    shell.insert(&plane, Anchor::Origin, ceiling);
    assert!(
        shell
            .bucket(&plane, Anchor::After(ceiling.into()))
            .is_none()
    );
    // A child anchored at the ceiling stores explicitly: no successor
    // exists for the plane to spell it with.
    let child = d(6, 1);
    let anchor = Anchor::After(ceiling.into());
    let value = Locus {
        anchor,
        rank: rank(2),
    };
    assert!(plane.insert(child, value));
    shell.insert(&plane, anchor, child);
    let bucket = shell.bucket(&plane, anchor).expect("the child is indexed");
    assert!(matches!(bucket, Bucket::Explicit(_)));
    assert_agrees(&shell, &plane);
}

#[test]
fn an_implicit_child_departs_with_its_plane_entry() {
    let mut plane = IdentityPlane::new();
    let mut shell = ChildPlane::new();
    weave_chain(&mut plane, &mut shell, 2, 5);
    // Excise the sterile tail: nothing is stored for it here, and the
    // endpoint-replacement read still reports the emptied bucket.
    let tail = d(2, 5);
    let removed = plane.remove(tail).expect("the tail was woven");
    let last_changed = shell.remove(&plane, removed.anchor, tail);
    assert_eq!(
        last_changed,
        TailChange::Replaced(None),
        "the tail was last; the bucket emptied"
    );
    assert!(
        shell
            .bucket(
                &plane,
                Anchor::After(RawDot {
                    station: 2,
                    counter: 4
                })
            )
            .is_none()
    );
    assert_agrees(&shell, &plane);
}

#[test]
fn a_self_anchored_dot_stores_explicitly() {
    // The wire tolerates a self-anchored locus (the S200 placement
    // finding); its bucket keys its own anchor and cannot be its own
    // chain child (a chain child succeeds its anchor's dot).
    let mut plane = IdentityPlane::new();
    let mut shell = ChildPlane::new();
    let dot = d(4, 2);
    let anchor = Anchor::After(dot.into());
    let value = Locus {
        anchor,
        rank: rank(3),
    };
    assert!(plane.insert(dot, value));
    shell.insert(&plane, anchor, dot);
    let bucket = shell
        .bucket(&plane, anchor)
        .expect("the self-anchor is indexed");
    assert!(matches!(bucket, Bucket::Explicit(_)));
    assert_eq!(bucket.first(), dot);
    assert_agrees(&shell, &plane);
}