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};
#[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,
)
}
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! {
#[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)));
}
}
}
#[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);
}
#[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:?}");
}
}
#[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);
}
}
#[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);
}
}
#[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);
}
}
}