minerva 0.2.0

Causal ordering for distributed systems
extern crate alloc;

use alloc::vec::Vec;

use proptest::prelude::*;

use crate::metis::{
    Anchor, Cut, Dot, DotSet, Dotted, Metatheses, RefoundMap, RefoundMapDecodeBudget,
    RefoundMapDecodeError,
};

use super::{Seq, clock, d, delete, insert};

/// One generated document step: a station pick, an anchor pick over the
/// dots woven so far (with its side), and whether the element is later
/// deleted. Random sided anchors scramble the walk order against the dot
/// order, so the generated maps carry genuine permutations; deletions
/// open ceiling-over-live gaps, swept stations, and refused translations.
#[derive(Clone, Debug)]
struct Step {
    station: u32,
    anchor: prop::sample::Index,
    before: bool,
    deleted: bool,
}

fn arb_steps() -> impl Strategy<Value = Vec<Step>> {
    prop::collection::vec(
        (
            1u32..=3,
            any::<prop::sample::Index>(),
            any::<bool>(),
            any::<bool>(),
        )
            .prop_map(|(station, anchor, before, deleted)| Step {
                station,
                anchor,
                before,
                deleted,
            }),
        0..24,
    )
}

/// Builds a document from the steps and folds it: every map this suite
/// round-trips is earned from a real re-foundation.
fn build_map(steps: &[Step]) -> RefoundMap {
    let clocks = [clock(1), clock(2), clock(3)];
    let mut replica: Seq = Dotted::new();
    let mut dots: Vec<Dot> = Vec::new();
    let mut doomed: Vec<Dot> = Vec::new();
    for step in steps {
        let anchor = if dots.is_empty() {
            Anchor::Origin
        } else {
            let &target = step.anchor.get(&dots);
            if step.before {
                Anchor::Before(target.into())
            } else {
                Anchor::After(target.into())
            }
        };
        let clk = &clocks[(step.station - 1) as usize];
        let dot = insert(&mut replica, clk, step.station, anchor);
        dots.push(dot);
        if step.deleted {
            doomed.push(dot);
        }
    }
    for dot in doomed {
        delete(&mut replica, dot);
    }

    let refounded = replica
        .store()
        .refound(&Metatheses::new())
        .expect("a fully placed, move-free stratum folds");
    let (_, map) = refounded.into_parts();
    map
}

proptest! {
    /// Encode-decode identity: `from_bytes(to_bytes(m)) == m` for every
    /// earned map, every accepted frame re-encodes to exactly its own
    /// bytes (the canonical bijection), and the decoded map translates
    /// identically across the whole compacted domain and the first
    /// stretch of each affine window.
    #[test]
    fn prop_refound_map_bytes_round_trip(steps in arb_steps()) {
        let map = build_map(&steps);
        let bytes = map.to_bytes();
        let decoded = RefoundMap::from_bytes(&bytes).expect("own frame decodes");
        prop_assert_eq!(&decoded, &map);
        prop_assert_eq!(decoded.to_bytes(), bytes);
        for station in 1..=3u32 {
            for dot in 1..=32u64 {
                prop_assert_eq!(decoded.translate(d(station, dot)), map.translate(d(station, dot)));
            }
        }
    }

    /// A cut-bound map (ceilings raised past the woven high water by a
    /// witnessed cut) rides the same rows and round-trips.
    #[test]
    fn prop_refound_map_cut_bound_round_trip(steps in arb_steps(), extra in 1u64..=4) {
        let mut map = build_map(&steps);
        let mut have = DotSet::new();
        for station in 1..=3u32 {
            let mut ceiling = 0;
            for dot in 1..=28u64 {
                if map.translate(d(station, dot)).is_some() {
                    ceiling = dot;
                }
            }
            for dot in 1..=(ceiling + extra) {
                let _ = have.insert(d(station, dot));
            }
        }
        map.bind_cut(&Cut::floor_of(&have));

        let bytes = map.to_bytes();
        let decoded = RefoundMap::from_bytes(&bytes).expect("a cut-bound frame decodes");
        prop_assert_eq!(&decoded, &map);
        prop_assert_eq!(decoded.to_bytes(), bytes);
    }

    /// The budgeted door agrees with the exact door whenever both budgets
    /// admit the frame, and refuses with the typed overflow when either
    /// does not.
    #[test]
    fn prop_refound_map_budget_is_exact(steps in arb_steps()) {
        let map = build_map(&steps);
        let bytes = map.to_bytes();
        let stations = bytes[1..9].iter().fold(0usize, |acc, &b| acc * 256 + b as usize);
        let entries = map.live_len();
        prop_assert_eq!(
            RefoundMap::from_bytes_with_budget(
                &bytes,
                RefoundMapDecodeBudget::new(stations, entries),
            ),
            Ok(map)
        );
        if stations > 0 {
            prop_assert_eq!(
                RefoundMap::from_bytes_with_budget(
                    &bytes,
                    RefoundMapDecodeBudget::new(stations - 1, entries),
                ),
                Err(RefoundMapDecodeError::TooManyStations {
                    count: stations as u64,
                    budget: stations as u64 - 1,
                })
            );
        }
        if entries > 0 {
            let refused = RefoundMap::from_bytes_with_budget(
                &bytes,
                RefoundMapDecodeBudget::new(stations, entries - 1),
            );
            let typed = matches!(
                refused,
                Err(RefoundMapDecodeError::TooManyEntries { budget, .. })
                    if budget == entries as u64 - 1
            );
            prop_assert!(typed, "expected the cumulative entry refusal, got {refused:?}");
        }
    }

    /// Decode never panics on arbitrary bytes, and every accepted frame
    /// re-encodes to exactly the bytes it decoded from.
    #[test]
    fn prop_refound_map_from_bytes_never_panics(
        bytes in prop::collection::vec(any::<u8>(), 0..192),
    ) {
        if let Ok(map) = RefoundMap::from_bytes(&bytes) {
            prop_assert_eq!(map.to_bytes(), bytes);
        }
    }

    /// Truncating a valid frame at every prefix length never panics, and
    /// any accepted prefix re-encodes to the bytes it consumed.
    #[test]
    fn prop_refound_map_truncation_never_panics(steps in arb_steps(), keep in any::<usize>()) {
        let bytes = build_map(&steps).to_bytes();
        let cut = keep % (bytes.len() + 1);
        let prefix = &bytes[..cut];
        if let Ok(map) = RefoundMap::from_bytes(prefix) {
            let reencoded = map.to_bytes();
            prop_assert_eq!(reencoded.as_slice(), prefix);
        }
    }

    /// Shaped totality on mutated valid frames: flipping one byte keeps
    /// the decoder total, and any accepted mutant re-encodes to exactly
    /// its own bytes.
    #[test]
    fn prop_refound_map_flip_byte_stays_total(
        steps in arb_steps(),
        offset in any::<usize>(),
        xor in 1u8..=u8::MAX,
    ) {
        let mut bytes = build_map(&steps).to_bytes();
        let len = bytes.len();
        bytes[offset % len] ^= xor;
        if let Ok(map) = RefoundMap::from_bytes(&bytes) {
            prop_assert_eq!(&map.to_bytes(), &bytes);
        }
    }
}