minerva 0.2.0

Causal ordering for distributed systems
extern crate alloc;

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

/// Arbitrary stamps for the envelope round-trip, across the full field widths.
fn arb_kairos() -> impl Strategy<Value = Kairos> {
    (any::<u64>(), any::<u16>(), any::<u32>(), any::<u16>()).prop_map(
        |(physical, logical, station_id, kairotic)| {
            Kairos::new(physical, logical, station_id, kairotic)
        },
    )
}

proptest! {
    /// The Event envelope (stamp, deps) survives concatenate-then-split-decode for
    /// arbitrary stamps and vectors, and the payload tail comes back untouched (R7).
    #[test]
    fn prop_envelope_round_trips(
        stamp in arb_kairos(),
        deps in arb_vv(),
        payload in prop::collection::vec(any::<u8>(), 0..16),
    ) {
        let mut buf = Vec::new();
        buf.extend_from_slice(&stamp.to_bytes());
        buf.extend_from_slice(&deps.to_bytes());
        buf.extend_from_slice(&payload);

        let decoded_stamp = Kairos::from_bytes(&buf[..KAIROS_WIRE_LEN]).unwrap();
        let (decoded_deps, tail) =
            VersionVector::from_prefix(&buf[KAIROS_WIRE_LEN..]).unwrap();

        prop_assert_eq!(decoded_stamp, stamp);
        prop_assert_eq!(decoded_deps, deps);
        prop_assert_eq!(tail, payload.as_slice());
    }

    /// The composed envelope decode (stamp frame, then `from_prefix`) is total over
    /// arbitrary bytes: neither parser panics, an accepted frame re-encodes to the
    /// exact bytes it consumed (byte identity, the property signature preimages and
    /// wire protocols rely on), and the tail comes back as the untouched suffix.
    /// The fuzz target `envelope_from_prefix` drives the same invariants far deeper.
    #[test]
    fn prop_envelope_from_prefix_never_panics(
        bytes in prop::collection::vec(any::<u8>(), 0..96),
    ) {
        if let Some(stamp_bytes) = bytes.get(..KAIROS_WIRE_LEN) {
            if let Ok(stamp) = Kairos::from_bytes(stamp_bytes) {
                let reencoded = stamp.to_bytes();
                prop_assert_eq!(reencoded.as_slice(), stamp_bytes);
            }
            if let Ok((deps, tail)) = VersionVector::from_prefix(&bytes[KAIROS_WIRE_LEN..]) {
                let end = bytes.len() - tail.len();
                let reencoded = deps.to_bytes();
                prop_assert_eq!(reencoded.as_slice(), &bytes[KAIROS_WIRE_LEN..end]);
                prop_assert_eq!(tail, &bytes[end..]);
            }
        } else {
            // Too short for the composition to begin; the vector parser must still
            // be panic-free over the whole input.
            let _ = VersionVector::from_prefix(&bytes);
        }
    }
}