minerva 0.2.0

extern crate alloc;

use alloc::vec::Vec;

use proptest::prelude::*;

use crate::kairos::Kairos;
use crate::metis::{
    Anchor, Locus, Metatheses, MetathesesDecodeBudget, MetathesesDecodeError, Metathesis,
};

/// One generated testimony row: a testimony dot, a target pick, an anchor
/// pick, and a rank tick. Target and anchor dots range over the same small
/// space as testimony dots *plus* the zero index, so the representable
/// zero-dot payloads are generated (they must round-trip).
#[derive(Clone, Debug)]
struct Row {
    station: u32,
    index: u64,
    target: (u32, u64),
    anchor: Option<((u32, u64), bool)>,
    tick: u64,
}

fn arb_rows() -> impl Strategy<Value = Vec<Row>> {
    prop::collection::vec(
        (
            1u32..=3,
            1u64..=8,
            (1u32..=3, 0u64..=8),
            prop::option::of(((1u32..=3, 0u64..=8), any::<bool>())),
            0u64..64,
        )
            .prop_map(|(station, index, target, anchor, tick)| Row {
                station,
                index,
                target,
                anchor,
                tick,
            }),
        0..24,
    )
}

/// Builds a record by inserting every row; a repeated testimony dot is
/// refused by `insert` (a dot names one write), so the record holds each
/// distinct dot once. Ranks are distinct per step so the value is fully
/// determined.
fn build(rows: &[Row]) -> Metatheses {
    let mut record = Metatheses::new();
    for (ordinal, row) in rows.iter().enumerate() {
        let anchor = match row.anchor {
            None => Anchor::Origin,
            Some((dot, false)) => Anchor::After(dot.into()),
            Some((dot, true)) => Anchor::Before(dot.into()),
        };
        let _ = record.insert(
            // The generated index starts at one, so it is always a dot.
            super::d(row.station, row.index),
            Metathesis {
                target: row.target.into(),
                to: Locus {
                    anchor,
                    rank: Kairos::new(row.tick * 64 + ordinal as u64, 0u16, row.station, 0u16),
                },
            },
        );
    }
    record
}

proptest! {
    /// Encode-decode identity: `from_bytes(to_bytes(m)) == m` for every
    /// generated record, and every accepted frame re-encodes to exactly
    /// its own bytes (the canonical bijection).
    #[test]
    fn prop_metatheses_bytes_round_trip(rows in arb_rows()) {
        let record = build(&rows);
        let bytes = record.to_bytes();
        let decoded = Metatheses::from_bytes(&bytes).expect("own frame decodes");
        prop_assert_eq!(&decoded, &record);
        prop_assert_eq!(decoded.to_bytes(), bytes);
    }

    /// The allocation-free length preflight reports exactly the emitted
    /// frame's length (S280: the embedding door's bounded admission, so a
    /// carrier never re-derives the row widths downstream).
    #[test]
    fn prop_metatheses_encoded_len_is_exact(rows in arb_rows()) {
        let record = build(&rows);
        prop_assert_eq!(record.encoded_len(), record.to_bytes().len());
    }

    /// Canonical: equal records encode to equal bytes. We reverse the
    /// insertion history; when both builds land on the same value, byte
    /// equality must follow.
    #[test]
    fn prop_metatheses_bytes_are_canonical(rows in arb_rows()) {
        let forward = build(&rows);
        let mut reversed = rows;
        reversed.reverse();
        let backward = build(&reversed);
        if forward == backward {
            prop_assert_eq!(forward.to_bytes(), backward.to_bytes());
        }
    }

    /// The budgeted door agrees with the exact door whenever the budget
    /// admits the count, and refuses with the typed overflow when it does
    /// not.
    #[test]
    fn prop_metatheses_budget_is_exact(rows in arb_rows()) {
        let record = build(&rows);
        let bytes = record.to_bytes();
        let len = record.len();
        prop_assert_eq!(
            Metatheses::from_bytes_with_budget(&bytes, MetathesesDecodeBudget::new(len)),
            Ok(record)
        );
        if len > 0 {
            prop_assert_eq!(
                Metatheses::from_bytes_with_budget(
                    &bytes,
                    MetathesesDecodeBudget::new(len - 1)
                ),
                Err(MetathesesDecodeError::TooManyTestimonies {
                    count: len as u64,
                    budget: len as u64 - 1,
                })
            );
        }
    }

    /// Decode never panics on arbitrary bytes, and every accepted frame
    /// re-encodes to exactly the bytes it decoded from.
    #[test]
    fn prop_metatheses_from_bytes_never_panics(
        bytes in prop::collection::vec(any::<u8>(), 0..192),
    ) {
        if let Ok(record) = Metatheses::from_bytes(&bytes) {
            prop_assert_eq!(record.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_metatheses_truncation_never_panics(rows in arb_rows(), keep in any::<usize>()) {
        let bytes = build(&rows).to_bytes();
        let cut = keep % (bytes.len() + 1);
        let prefix = &bytes[..cut];
        if let Ok(record) = Metatheses::from_bytes(prefix) {
            let reencoded = record.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_metatheses_flip_byte_stays_total(
        rows in arb_rows(),
        offset in any::<usize>(),
        xor in 1u8..=u8::MAX,
    ) {
        let mut bytes = build(&rows).to_bytes();
        let len = bytes.len();
        bytes[offset % len] ^= xor;
        if let Ok(record) = Metatheses::from_bytes(&bytes) {
            prop_assert_eq!(&record.to_bytes(), &bytes);
        }
    }
}