minerva 0.2.0

extern crate std;

use super::super::Anchor;
use super::*;
use crate::kairos::{Clock, Kairos, TickCounter};
use crate::metis::dot::RawDot;
use proptest::prelude::*;

/// A literal identity for the tapes below (test machinery: every counter
/// drawn here is one-based, so the crossing never refuses).
fn d(station: u32, counter: u64) -> Dot {
    Dot::from_parts(station, counter).expect("a test dot has a nonzero counter")
}

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

/// A chain of `len` consecutive dots for `station` starting at index
/// `base`, each anchored after its predecessor with the rank stepping
/// by the given per-element steps (zero is the clock successor), i.e.
/// exactly the shape the plane coalesces.
fn chain(station: u32, base: u64, steps: &[u64]) -> Vec<(Dot, Locus)> {
    let mut out = Vec::with_capacity(steps.len() + 1);
    let head_dot = d(station, base);
    let head = Locus {
        anchor: Anchor::Origin,
        rank: Kairos::new(1_000, 5, station, 7u16),
    };
    out.push((head_dot, head));
    let (mut prev_dot, mut prev) = (head_dot, head);
    for &step in steps {
        let dot = d(station, prev_dot.counter() + 1);
        let next = apply_chain_step(prev_dot.into(), &prev, step);
        out.push((dot, next));
        (prev_dot, prev) = (dot, next);
    }
    out
}

/// One step of a plane's life: a keyed write or a keyed removal, plus
/// the chain append that exercises the coalesced spelling. Indices mix
/// a dense low range (the honest mint shape) with the far top of the
/// dot space (the adversarial-decode shape), so tapes exercise prefix
/// pages, exception pages, promotion, freeing, handle reuse, step
/// spelling, and follower re-materialization.
#[derive(Clone, Debug)]
enum Op {
    Insert { station: u32, index: u64, salt: u16 },
    Extend { station: u32, step: u64, gap: bool },
    Remove { station: u32, index: u64 },
}

/// The tape's index domain. The non-dot `0` no longer appears: [`Dot`]
/// carries that law, so the arm is unrepresentable rather than exercised
/// (ruling R-91).
fn arb_index() -> impl Strategy<Value = u64> {
    prop_oneof![
        4 => 1..=(3 * PAGE_LEN_U64),
        1 => (u64::MAX - 2 * PAGE_LEN_U64)..=u64::MAX,
    ]
}

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

fn hash_of(plane: &IdentityPlane) -> u64 {
    use core::hash::{Hash, Hasher};
    let mut h = std::collections::hash_map::DefaultHasher::new();
    plane.hash(&mut h);
    h.finish()
}

proptest! {
    /// The dual-form agreement pin the shell discipline demands (its rule:
    /// no shell ships without one). Over any op tape, the coalesced plane
    /// and the `BTreeMap` contract form agree on every observation: each
    /// step's verdict, the final length, the ascending enumeration, and
    /// every point read. And the layout stays out of the value: a plane
    /// rebuilt straight from the surviving entries (fresh handles, fresh
    /// step spellings, no free-list history, no exception pages) is equal
    /// to the churned one and hashes identically.
    #[test]
    fn prop_plane_agrees_with_the_map_form(
        ops in prop::collection::vec(arb_op(), 0..160),
    ) {
        let clock = Clock::with_default_config(TickCounter::new(), 1)
            .expect("test clock config");
        let mut plane = IdentityPlane::new();
        let mut model: BTreeMap<Dot, Locus> = BTreeMap::new();
        // Per-station chain tails for `Extend`: the next fresh index and
        // whether the predecessor's locus still stands in the model.
        let mut tails: BTreeMap<u32, u64> = BTreeMap::new();
        for op in &ops {
            match *op {
                Op::Insert { station, index, salt } => {
                    let anchor = match salt % 3 {
                        0 => Anchor::Origin,
                        1 => Anchor::After(RawDot { station, counter: u64::from(salt) + 1 }),
                        _ => Anchor::Before(RawDot { station, counter: u64::from(salt) + 1 }),
                    };
                    let value = Locus { anchor, rank: clock.now(salt) };
                    let fresh_model = !model.contains_key(&d(station, index));
                    if fresh_model {
                        let _ = model.insert(d(station, index), value);
                    }
                    prop_assert_eq!(plane.insert(d(station, index), value), fresh_model);
                }
                Op::Extend { station, step, gap } => {
                    let tail = tails.entry(station).or_insert(1);
                    if gap {
                        *tail += 1;
                    }
                    let index = *tail;
                    let prev_dot = (station, index.wrapping_sub(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 fresh_model = !model.contains_key(&d(station, index));
                    if fresh_model {
                        let _ = model.insert(d(station, index), value);
                    }
                    prop_assert_eq!(plane.insert(d(station, index), value), fresh_model);
                    *tail += 1;
                }
                Op::Remove { station, index } => {
                    prop_assert_eq!(
                        plane.remove(d(station, index)),
                        model.remove(&d(station, index)),
                    );
                }
            }
        }
        prop_assert_eq!(plane.len(), model.len());
        prop_assert!(plane.is_empty() == model.is_empty());
        prop_assert!(
            plane
                .iter()
                .eq(model.iter().map(|(&dot, &value)| (dot, value))),
            "the ascending enumerations disagree",
        );
        for (dot, value) in &model {
            prop_assert!(plane.contains(*dot));
            prop_assert_eq!(plane.get(dot), Some(*value));
        }
        // Layout out of the value: the straight rebuild is the same plane.
        let mut straight = IdentityPlane::new();
        for (&dot, &value) in &model {
            prop_assert!(straight.insert(dot, value));
        }
        prop_assert_eq!(&plane, &straight);
        prop_assert_eq!(hash_of(&plane), hash_of(&straight));
    }
}

proptest! {
    /// The run insert is the per-dot fold, exactly: over any mix of
    /// point inserts, removals, and chain-run bulk inserts (page
    /// -spanning, occupied-slot-refused, unchainable-rank shapes
    /// included), the bulk plane and a per-dot twin agree on every
    /// verdict, every read, and the canonical value; and the bulk
    /// verdict is all-or-nothing (a refused run changes nothing).
    #[test]
    fn prop_insert_run_agrees_with_the_per_dot_fold(
        ops in prop::collection::vec(
            prop_oneof![
                2 => (0..3u32, 1..200u64, any::<u16>())
                    .prop_map(|(station, index, salt)| (station, index, salt, 0usize)),
                2 => (0..3u32, 1..200u64, any::<u16>(), 1..150usize)
                    .prop_map(|(station, first, salt, len)| (station, first, salt, len)),
                1 => (0..3u32, 1..200u64)
                    .prop_map(|(station, index)| (station, index, 0u16, usize::MAX)),
            ],
            0..24,
        ),
    ) {
        let mut bulk = IdentityPlane::new();
        let mut pointwise = IdentityPlane::new();
        for &(station, first, salt, kind) in &ops {
            match kind {
                // A removal on both planes.
                usize::MAX => {
                    prop_assert_eq!(
                        bulk.remove(d(station, first)),
                        pointwise.remove(d(station, first)),
                    );
                }
                // A point insert on both planes.
                0 => {
                    let anchor = match salt % 3 {
                        0 => Anchor::Origin,
                        1 => Anchor::After(RawDot { station, counter: u64::from(salt) + 1 }),
                        _ => Anchor::Before(RawDot { station, counter: u64::from(salt) + 1 }),
                    };
                    let value = Locus { anchor, rank: Kairos::new(u64::from(salt), 0, station.max(1), salt) };
                    prop_assert_eq!(
                        bulk.insert(d(station, first), value),
                        pointwise.insert(d(station, first), value),
                    );
                }
                // A chain run: the head anchored per salt, interiors
                // chained with a salted step (zero is the successor;
                // an occasional wide step exercises the explicit
                // fallback inside a run).
                len => {
                    let head = Locus {
                        anchor: if salt % 2 == 0 {
                            Anchor::Origin
                        } else {
                            Anchor::After(RawDot { station, counter: u64::from(salt) })
                        },
                        rank: Kairos::new(1_000 + u64::from(salt), 3, station.max(1), salt),
                    };
                    let mut loci = Vec::with_capacity(len);
                    loci.push(head);
                    let (mut prev_dot, mut prev) = ((station, first), head);
                    for k in 1..len {
                        let step = match (salt as usize + k) % 7 {
                            0 => 4,
                            1 => u64::from(u32::MAX),
                            _ => 0,
                        };
                        let next = apply_chain_step(prev_dot, &prev, step);
                        loci.push(next);
                        prev_dot = (station, first + k as u64);
                        prev = next;
                    }
                    let before = bulk.clone();
                    let verdict = bulk.insert_run(d(station, first), &loci);
                    // The per-dot twin folds the same entries one at a
                    // time; the bulk verdict is true iff every per-dot
                    // verdict would be (freshness of the whole range).
                    let mut all_fresh = true;
                    for k in 0..loci.len() {
                        all_fresh &= !pointwise.contains(d(station, first + k as u64));
                    }
                    if all_fresh {
                        prop_assert!(verdict);
                        for (k, &value) in loci.iter().enumerate() {
                            prop_assert!(pointwise.insert(d(station, first + k as u64), value));
                        }
                    } else {
                        prop_assert!(!verdict, "an occupied slot refuses the whole run");
                        prop_assert_eq!(&bulk, &before, "a refused run changes nothing");
                    }
                }
            }
            prop_assert_eq!(&bulk, &pointwise);
            prop_assert_eq!(bulk.len(), pointwise.len());
        }
        prop_assert!(bulk.iter().eq(pointwise.iter()));
    }
}

#[test]
fn test_a_bulk_run_spells_like_the_per_dot_fold() {
    // The spelling itself agrees, not just the value: a bulk chain run
    // and the same entries folded per dot intern the same explicit
    // count (heads and page boundaries explicit, interiors stepped).
    let entries = chain(2, 63, &alloc::vec![0u64; 130]);
    let mut bulk = IdentityPlane::new();
    let loci: Vec<Locus> = entries.iter().map(|&(_, locus)| locus).collect();
    assert!(bulk.insert_run(d(2, 63), &loci));
    let mut pointwise = IdentityPlane::new();
    for &(dot, value) in &entries {
        assert!(pointwise.insert(dot, value));
    }
    assert_eq!(bulk, pointwise);
    assert_eq!(bulk.explicit_entries(), pointwise.explicit_entries());
    // Dot 63 is slot 62 of page 0; dots 65, 129, and 193 are page
    // heads: the run pays exactly one entry plus its page-boundary
    // heads.
    assert_eq!(bulk.explicit_entries(), 4);
}

#[test]
fn test_a_run_refuses_the_ceiling_and_the_cap_whole() {
    let mut plane = IdentityPlane::new();
    let entries = chain(1, 1, &[0, 0]);
    let loci: Vec<Locus> = entries.iter().map(|&(_, locus)| locus).collect();
    // A run that would pass the dot ceiling refuses outright.
    assert!(!plane.insert_run(d(1, u64::MAX - 1), &loci));
    assert!(plane.is_empty(), "a refused run changes nothing");
    // The non-dot zero is unrepresentable now: [`Dot`] carries the law
    // (ruling R-91), so there is no arm left to exercise.
    // The empty run refuses.
    assert!(!plane.insert_run(d(1, 5), &[]));
    assert!(plane.is_empty());
}

#[test]
fn a_chain_run_shares_one_column_entry() {
    let mut plane = IdentityPlane::new();
    let entries = chain(3, 1, &[0, 0, 4, 0, 0, 0, 250, 0, 0]);
    for &(dot, value) in &entries {
        assert!(plane.insert(dot, value));
    }
    assert_eq!(plane.len(), entries.len());
    assert_eq!(plane.column_len(), 1, "the interior rode inline");
    assert_eq!(plane.explicit_entries(), 1);
    for &(dot, value) in &entries {
        assert_eq!(plane.get(&dot), Some(value), "point reads are exact");
    }
    assert!(plane.iter().eq(entries.iter().copied()));
}

#[test]
fn a_page_boundary_re_materializes_the_chain() {
    let mut plane = IdentityPlane::new();
    let steps = alloc::vec![0u64; 2 * PAGE_LEN];
    let entries = chain(1, 1, &steps);
    for &(dot, value) in &entries {
        assert!(plane.insert(dot, value));
    }
    // Slot zero of each touched page is explicit: dots 1, 65, and 129.
    assert_eq!(plane.explicit_entries(), 3);
    for &(dot, value) in &entries {
        assert_eq!(plane.get(&dot), Some(value));
    }
}

#[test]
fn removing_a_predecessor_re_materializes_the_follower() {
    let mut plane = IdentityPlane::new();
    let entries = chain(2, 1, &[0, 3, 0]);
    for &(dot, value) in &entries {
        assert!(plane.insert(dot, value));
    }
    assert_eq!(plane.explicit_entries(), 1);
    // Excise the interior dot 2: dot 3's step derived from it, so dot 3
    // must come out explicit while dots 1 and 4 keep their spellings.
    assert_eq!(plane.remove(d(2, 2)), Some(entries[1].1));
    assert_eq!(plane.len(), 3);
    assert_eq!(plane.explicit_entries(), 2, "the follower was re-homed");
    assert_eq!(plane.get(&d(2, 1)), Some(entries[0].1));
    assert!(!plane.contains(d(2, 2)));
    assert_eq!(plane.get(&d(2, 3)), Some(entries[2].1));
    assert_eq!(plane.get(&d(2, 4)), Some(entries[3].1));
    // And the head's removal re-homes the once-stepped dot 3's follower
    // chain likewise.
    assert_eq!(plane.remove(d(2, 1)), Some(entries[0].1));
    assert_eq!(plane.get(&d(2, 3)), Some(entries[2].1));
    assert_eq!(plane.get(&d(2, 4)), Some(entries[3].1));
}

#[test]
fn an_unchainable_entry_stays_explicit() {
    let mut plane = IdentityPlane::new();
    let head_dot = d(1, 1);
    let head = Locus {
        anchor: Anchor::Origin,
        rank: Kairos::new(1_000, 0, 1, 7u16),
    };
    assert!(plane.insert(head_dot, head));
    // Consecutive dot, but anchored Before: the chain law refuses.
    let sided = Locus {
        anchor: Anchor::Before(head_dot.into()),
        rank: Kairos::new(1_001, 0, 1, 7u16),
    };
    assert!(plane.insert(d(1, 2), sided));
    // Consecutive dot, After, but a foreign kairotic: refused too.
    let foreign = Locus {
        anchor: Anchor::After(RawDot {
            station: 1,
            counter: 2,
        }),
        rank: Kairos::new(1_002, 0, 1, 9u16),
    };
    assert!(plane.insert(d(1, 3), foreign));
    // Consecutive dot, After, but the physical advance is past the
    // slot's 31-bit payload: a genuine chain that stays explicit (the
    // layout fallback the value never sees).
    let wide = Locus {
        anchor: Anchor::After(RawDot {
            station: 1,
            counter: 3,
        }),
        rank: Kairos::new(1_002 + u64::from(u32::MAX), 0, 1, 9u16),
    };
    assert!(plane.insert(d(1, 4), wide));
    assert_eq!(plane.explicit_entries(), 4);
    assert_eq!(plane.get(&d(1, 2)), Some(sided));
    assert_eq!(plane.get(&d(1, 3)), Some(foreign));
    assert_eq!(plane.get(&d(1, 4)), Some(wide));
}

#[test]
fn sparse_far_dot_allocates_one_page() {
    let mut plane = IdentityPlane::new();
    let far = d(7, u64::MAX);
    assert!(plane.insert(far, locus(Anchor::Origin, 0)));

    assert_eq!(plane.len(), 1);
    assert_eq!(plane.pages_allocated(), 1);
    assert_eq!(plane.column_len(), 1);
    assert!(plane.contains(far));
    assert_eq!(plane.iter().map(|(dot, _)| dot).collect::<Vec<_>>(), [far]);
}

#[test]
fn equality_ignores_free_list_and_spelling_history() {
    let a = d(1, 1);
    let b = d(1, 2);
    let la = locus(Anchor::Origin, 0);
    let lb = locus(Anchor::After(a.into()), 1);

    let mut churned = IdentityPlane::new();
    assert!(churned.insert(a, la));
    assert!(churned.insert(b, lb));
    assert!(churned.remove(a).is_some());
    assert!(churned.insert(a, la));

    let mut straight = IdentityPlane::new();
    assert!(straight.insert(a, la));
    assert!(straight.insert(b, lb));

    assert_eq!(churned, straight);
    assert_eq!(churned.column_len(), straight.column_len());

    // The step spelling is layout too: a chain inserted tail-first holds
    // explicit entries where the ascending rebuild steps, and the two
    // planes are one value.
    let entries = chain(4, 1, &[0, 2, 0]);
    let mut backward = IdentityPlane::new();
    for &(dot, value) in entries.iter().rev() {
        assert!(backward.insert(dot, value));
    }
    let mut forward = IdentityPlane::new();
    for &(dot, value) in &entries {
        assert!(forward.insert(dot, value));
    }
    assert!(backward.explicit_entries() > forward.explicit_entries());
    assert_eq!(backward, forward);
    assert_eq!(hash_of(&backward), hash_of(&forward));
}

#[test]
fn removal_frees_pages_and_reuses_the_column_slot() {
    let mut plane = IdentityPlane::new();
    let first = d(2, 1);
    let second = d(2, PAGE_LEN as u64 + 1);
    assert!(plane.insert(first, locus(Anchor::Origin, 0)));
    assert!(plane.insert(second, locus(Anchor::After(first.into()), 1)));
    assert_eq!(plane.pages_allocated(), 2);
    assert_eq!(plane.column_len(), 2);

    let removed = plane.remove(second).expect("second dot was present");
    assert_eq!(removed.anchor, Anchor::After(first.into()));
    assert_eq!(plane.pages_allocated(), 1);
    assert_eq!(plane.column_len(), 2);

    let replacement = d(3, 1);
    assert!(plane.insert(replacement, locus(Anchor::After(first.into()), 2),));
    assert_eq!(plane.column_len(), 2, "the retired handle was reused");
    assert_eq!(
        plane.iter().map(|(dot, _)| dot).collect::<Vec<_>>(),
        [first, replacement],
    );
}