minerva 0.2.0

extern crate alloc;

use super::super::super::support::arb_vv;
use crate::metis::{DecodeError, VersionVector};
use alloc::vec::Vec;
use proptest::prelude::*;

/// A structured mutation of a valid frame. Uniform-random bytes almost never
/// reach the deep parser branches (a valid header is a 1-in-2^40 draw), so these
/// start from a canonical frame and break it one aspect at a time, the
/// generator-side counterpart of the branch-covering idea (S86, ruling R-9:
/// shaped sampling owns the map-touching parser laws that are out of Kani's
/// affordable scope).
#[derive(Debug, Clone)]
enum FrameMutation {
    /// Flip one byte anywhere in the frame.
    FlipByte { offset: usize, xor: u8 },
    /// Truncate the frame to a prefix.
    Truncate { keep: usize },
    /// Append junk, which `from_bytes` must reject and `from_prefix` must
    /// hand back untouched.
    Append(Vec<u8>),
}

fn arb_mutation() -> impl Strategy<Value = FrameMutation> {
    prop_oneof![
        (any::<usize>(), 1u8..=u8::MAX)
            .prop_map(|(offset, xor)| FrameMutation::FlipByte { offset, xor }),
        any::<usize>().prop_map(|keep| FrameMutation::Truncate { keep }),
        prop::collection::vec(any::<u8>(), 1..16).prop_map(FrameMutation::Append),
    ]
}

proptest! {
    /// Round-trip: decode inverts encode for every vector (R6).
    #[test]
    fn prop_vv_bytes_round_trip(v in arb_vv()) {
        prop_assert_eq!(v.encoded_len(), v.to_bytes().len());
        prop_assert_eq!(VersionVector::from_bytes(&v.to_bytes()), Ok(v));
    }

    /// Canonical bijection: redundant zero-observes encode to the same bytes (R2).
    #[test]
    fn prop_vv_bytes_are_canonical(
        v in arb_vv(),
        noise in prop::collection::vec(0u32..6, 0..4),
    ) {
        let mut other = v.clone();
        for station in noise {
            other.observe(station, 0);
        }
        prop_assert_eq!(&v, &other);
        prop_assert_eq!(v.to_bytes(), other.to_bytes());
    }

    /// Decode never panics on arbitrary bytes, and accepted frames re-encode identically.
    #[test]
    fn prop_vv_from_bytes_never_panics(bytes in prop::collection::vec(any::<u8>(), 0..64)) {
        if let Ok(v) = VersionVector::from_bytes(&bytes) {
            prop_assert_eq!(v.to_bytes(), bytes);
        }
    }

    /// Decode is total and byte-identical on *mutated valid frames*: start from a
    /// canonical encoding and flip, truncate, or extend it. This walks the
    /// near-valid input space where the deep branches live, which uniform-random
    /// bytes reach only with vanishing probability; an accepted mutant must
    /// re-encode to exactly the bytes it decoded from (the canonical bijection,
    /// R2/R4).
    #[test]
    fn prop_vv_decode_total_on_mutated_frames(
        v in arb_vv(),
        mutation in arb_mutation(),
    ) {
        let mut bytes = v.to_bytes();
        match mutation {
            FrameMutation::FlipByte { offset, xor } => {
                let len = bytes.len();
                bytes[offset % len] ^= xor;
            }
            FrameMutation::Truncate { keep } => {
                bytes.truncate(keep % (bytes.len() + 1));
            }
            FrameMutation::Append(junk) => bytes.extend_from_slice(&junk),
        }
        if let Ok(decoded) = VersionVector::from_bytes(&bytes) {
            let reencoded = decoded.to_bytes();
            prop_assert_eq!(&reencoded, &bytes);
        }
        if let Ok((prefix, tail)) = VersionVector::from_prefix(&bytes) {
            let consumed = bytes.len() - tail.len();
            let reencoded = prefix.to_bytes();
            prop_assert_eq!(reencoded.as_slice(), &bytes[..consumed]);
            prop_assert_eq!(tail, &bytes[consumed..]);
        }
    }

    /// The canonical-form rejections, shaped: a two-entry frame whose stations
    /// are non-ascending (unsorted or duplicate) or whose counter is zero is
    /// refused with the exact error naming the offense, never admitted and never
    /// panicking (R4). Shaped generation makes these branches certain per case
    /// instead of astronomically rare.
    #[test]
    fn prop_vv_rejects_shaped_non_canonical_frames(
        station_a in any::<u32>(),
        station_delta in any::<u32>(),
        counter_a in any::<u64>(),
        counter_b in any::<u64>(),
        break_order in any::<bool>(),
    ) {
        // Either break the strict ascent (station_b <= station_a) or zero a counter.
        let (station_b, counter_a, counter_b) = if break_order {
            (
                station_a.saturating_sub(station_delta),
                counter_a.max(1),
                counter_b.max(1),
            )
        } else {
            // Canonical order, but force a zero counter into one slot.
            let station_b = station_a.saturating_add((station_delta % 8) + 1);
            if station_delta.is_multiple_of(2) {
                (station_b, 0, counter_b)
            } else {
                (station_b, counter_a.max(1), 0)
            }
        };
        let mut bytes = Vec::with_capacity(29);
        bytes.push(0x01);
        bytes.extend_from_slice(&2u32.to_be_bytes());
        bytes.extend_from_slice(&station_a.to_be_bytes());
        bytes.extend_from_slice(&counter_a.to_be_bytes());
        bytes.extend_from_slice(&station_b.to_be_bytes());
        bytes.extend_from_slice(&counter_b.to_be_bytes());
        let result = VersionVector::from_bytes(&bytes);
        if counter_a == 0 {
            prop_assert_eq!(result, Err(DecodeError::ZeroCounter { station: station_a }));
        } else if break_order && station_b <= station_a {
            prop_assert_eq!(
                result,
                Err(DecodeError::NonAscendingStations {
                    previous: station_a,
                    found: station_b,
                })
            );
        } else if counter_b == 0 {
            prop_assert_eq!(result, Err(DecodeError::ZeroCounter { station: station_b }));
        } else {
            // Generator invariant: every shaped frame breaks exactly one rule
            // (saturating_sub makes non-ascent certain under break_order, and the
            // other arm force-zeroes a counter), so reaching here is a bug in the
            // generator, not the parser.
            prop_assert!(false, "shaped generator produced a canonical frame");
        }
    }
}