minerva 0.2.0

Causal ordering for distributed systems
extern crate alloc;

use crate::metis::{DotSet, HaveSetDecodeError};
use alloc::vec::Vec;
use proptest::prelude::*;

proptest! {
    #[test]
    fn prop_have_set_rejects_swapped_stations(
        floor_a in 1u64..8, floor_b in 1u64..8,
    ) {
        let mut bytes = Vec::new();
        bytes.push(0x01u8);
        bytes.extend_from_slice(&2u32.to_be_bytes());
        for (station, floor) in [(5u32, floor_a), (3u32, floor_b)] {
            bytes.extend_from_slice(&station.to_be_bytes());
            bytes.extend_from_slice(&floor.to_be_bytes());
            bytes.extend_from_slice(&0u32.to_be_bytes());
        }
        prop_assert_eq!(
            DotSet::from_bytes(&bytes),
            Err(HaveSetDecodeError::NonAscendingStations { previous: 5, found: 3 })
        );
    }

    #[test]
    fn prop_have_set_rejects_run_adjacent_to_floor(floor in 1u64..1_000, len in 1u64..8) {
        let mut bytes = Vec::new();
        bytes.push(0x01u8);
        bytes.extend_from_slice(&1u32.to_be_bytes());
        bytes.extend_from_slice(&1u32.to_be_bytes());
        bytes.extend_from_slice(&floor.to_be_bytes());
        bytes.extend_from_slice(&1u32.to_be_bytes());
        bytes.extend_from_slice(&(floor + 1).to_be_bytes());
        bytes.extend_from_slice(&len.to_be_bytes());
        prop_assert_eq!(
            DotSet::from_bytes(&bytes),
            Err(HaveSetDecodeError::NonMaximalRun { station: 1, start: floor + 1 })
        );
    }

    #[test]
    fn prop_have_set_rejects_adjacent_runs(
        floor in 1u64..100, first_start_gap in 1u64..8, first_len in 1u64..8,
    ) {
        let start1 = floor + 1 + first_start_gap;
        let end1 = start1 + first_len - 1;
        let start2 = end1 + 1;
        let mut bytes = Vec::new();
        bytes.push(0x01u8);
        bytes.extend_from_slice(&1u32.to_be_bytes());
        bytes.extend_from_slice(&1u32.to_be_bytes());
        bytes.extend_from_slice(&floor.to_be_bytes());
        bytes.extend_from_slice(&2u32.to_be_bytes());
        bytes.extend_from_slice(&start1.to_be_bytes());
        bytes.extend_from_slice(&first_len.to_be_bytes());
        bytes.extend_from_slice(&start2.to_be_bytes());
        bytes.extend_from_slice(&1u64.to_be_bytes());
        prop_assert_eq!(
            DotSet::from_bytes(&bytes),
            Err(HaveSetDecodeError::NonMaximalRun { station: 1, start: start2 })
        );
    }

    #[test]
    fn prop_have_set_rejects_zero_length_run(floor in 1u64..100, start_gap in 1u64..8) {
        let start = floor + 1 + start_gap;
        let mut bytes = Vec::new();
        bytes.push(0x01u8);
        bytes.extend_from_slice(&1u32.to_be_bytes());
        bytes.extend_from_slice(&1u32.to_be_bytes());
        bytes.extend_from_slice(&floor.to_be_bytes());
        bytes.extend_from_slice(&1u32.to_be_bytes());
        bytes.extend_from_slice(&start.to_be_bytes());
        bytes.extend_from_slice(&0u64.to_be_bytes());
        prop_assert_eq!(
            DotSet::from_bytes(&bytes),
            Err(HaveSetDecodeError::ZeroLengthRun { station: 1 })
        );
    }
}