minerva 0.2.0

extern crate alloc;

use core::num::NonZeroU64;

use super::super::super::support::dot;
use super::{arb_dots, have, model};
use crate::metis::{DotSet, DotStore};
use proptest::prelude::*;

proptest! {
    /// The run insert is the per-dot insert, exactly: over any interleaving
    /// of point inserts and run inserts (runs overlapping floors,
    /// exceptions, and prior runs), the run form and a twin inserting the
    /// same runs one dot at a time are one canonical value, including at
    /// the dot ceiling (where neither form can name a dot past `u64::MAX`).
    ///
    /// The zero case died with the type: `first` is a `NonZeroU64`, so the
    /// old `first.max(1)` clamp --- and the reshaped run it produced --- is
    /// unrepresentable (ruling R-91).
    #[test]
    fn prop_insert_run_agrees_with_the_per_dot_form(
        ops in prop::collection::vec(
            prop_oneof![
                (0u32..4, 1u64..12).prop_map(|(station, counter)| (station, counter, 1u32)),
                (0u32..4, 1u64..40, 1u32..24).prop_map(|(station, first, len)| (station, first, len)),
                // The ceiling shapes: runs starting at or truncating against u64::MAX.
                (0u32..4, (u64::MAX - 8)..=u64::MAX, 1u32..12)
                    .prop_map(|(station, first, len)| (station, first, len)),
            ],
            0..24,
        ),
    ) {
        let mut bulk = DotSet::new();
        let mut pointwise = DotSet::new();
        for &(station, first, len) in &ops {
            let first = NonZeroU64::new(first).expect("the generator draws first >= 1");
            bulk.insert_run(station, first, len);
            let last = first.get().saturating_add(u64::from(len) - 1);
            let mut counter = first.get();
            loop {
                let _ = pointwise.insert(dot(station, counter));
                if counter >= last {
                    break;
                }
                counter += 1;
            }
        }
        prop_assert_eq!(&bulk, &pointwise);
    }

    /// The type is an exact set: membership agrees with the reference model,
    /// and insertion order does not change canonical equality.
    #[test]
    fn prop_dot_set_is_an_exact_set(
        (dots, permuted) in arb_dots()
            .prop_flat_map(|d| (Just(d.clone()), Just(d).prop_shuffle())),
    ) {
        let set = have(&dots);
        let expected = model(&dots);
        // Counter zero is no dot, so the sweep starts at one: the arm that
        // read `contains(station, 0)` is unrepresentable (ruling R-91).
        for station in 0u32..4 {
            for counter in 1u64..13 {
                prop_assert_eq!(
                    set.contains(dot(station, counter)),
                    expected.contains(&dot(station, counter))
                );
            }
        }
        prop_assert_eq!(have(&permuted), set);
    }

    /// `merge` is the union join: membership-exact, commutative, associative,
    /// idempotent.
    #[test]
    fn prop_merge_is_the_union_join(
        a in arb_dots(), b in arb_dots(), c in arb_dots(),
    ) {
        let (sa, sb, sc) = (have(&a), have(&b), have(&c));
        let union = sa.merge(&sb);
        for station in 0u32..4 {
            for counter in 1u64..13 {
                prop_assert_eq!(
                    union.contains(dot(station, counter)),
                    sa.contains(dot(station, counter)) || sb.contains(dot(station, counter))
                );
            }
        }
        prop_assert_eq!(&union, &sb.merge(&sa));
        prop_assert_eq!(sa.merge(&sb).merge(&sc), sa.merge(&sb.merge(&sc)));
        prop_assert_eq!(sa.merge(&sa), sa);
    }
}

/// The ceiling canonicality corner the S212 gate review named: a run that
/// raises a station's floor to the absolute `u64::MAX` must ABSORB an
/// exception already parked at the ceiling, exactly as the per-dot form
/// does; a saturating split point would retain it beside the ceiling floor,
/// a duplicate representation. Unreachable through inserts alone (the
/// floor cannot climb to the ceiling one dot at a time in any test), so
/// the floor is seeded through the crate-internal witnessed-cut embedding.
#[test]
fn test_a_ceiling_run_absorbs_the_parked_ceiling_exception() {
    let mut cut = crate::metis::VersionVector::new();
    cut.observe(1, u64::MAX - 3);
    let mut bulk = DotSet::from_cut(&cut);
    let mut pointwise = bulk.clone();
    assert!(bulk.insert(dot(1, u64::MAX)));
    assert!(pointwise.insert(dot(1, u64::MAX)));
    assert_eq!(
        bulk.exceptions_len(),
        1,
        "the ceiling dot parks above the gap"
    );

    bulk.insert_run(
        1,
        NonZeroU64::new(u64::MAX - 2).expect("the ceiling minus two is nonzero"),
        3,
    );
    for counter in [u64::MAX - 2, u64::MAX - 1] {
        assert!(pointwise.insert(dot(1, counter)));
    }
    assert!(!pointwise.insert(dot(1, u64::MAX)), "already held");

    assert_eq!(bulk, pointwise);
    assert_eq!(
        bulk.floor().get(1),
        u64::MAX,
        "the floor reaches the ceiling"
    );
    assert_eq!(
        bulk.exceptions_len(),
        0,
        "the ceiling exception was absorbed, never duplicated"
    );
}

/// The ceiling removal corner the S349 gate review named: the survivor law
/// drops a dot AT a station's `u64::MAX` floor when a peer's context covers
/// the dot and its store no longer holds it. The retraction parks the old
/// prefix above the removed dot, and at the ceiling the unguarded range
/// start would compute `u64::MAX + 1`: a panic in checked builds, an
/// effectively unbounded parked range in unchecked ones. Unreachable
/// through inserts alone (the S212 rationale), so the floor is seeded
/// through the crate-internal witnessed-cut embedding.
#[test]
fn test_a_ceiling_removal_parks_no_range_past_the_ceiling() {
    let mut seen = crate::metis::VersionVector::new();
    seen.observe(1, u64::MAX);
    // This replica holds the whole prefix through the ceiling.
    let held = DotSet::from_cut(&seen);

    // The peer saw the same prefix (its context covers the ceiling dot)
    // and dropped exactly the ceiling dot from its store.
    let mut retained = crate::metis::VersionVector::new();
    retained.observe(1, u64::MAX - 1);
    let peer_store = DotSet::from_cut(&retained);
    let peer_context = held.clone();

    // The in-place fold's removal pass is the guarded path.
    let mut folded = held.clone();
    folded.causal_merge_from(&held, &peer_store, &peer_context);

    let rebuilt = held.causal_merge(&held, &peer_store, &peer_context);
    assert_eq!(
        folded, rebuilt,
        "in-place fold agrees with the pure rebuild"
    );
    assert_eq!(
        folded.floor().get(1),
        u64::MAX - 1,
        "the floor retracts one dot, canonically"
    );
    assert!(!folded.contains(dot(1, u64::MAX)), "the ceiling dot died");
    assert_eq!(
        folded.exceptions_len(),
        0,
        "no parked range crosses the ceiling"
    );
}