use proptest::prelude::*;
use super::*;
use crate::metis::dot::RawDot;
proptest! {
#![proptest_config(ProptestConfig::with_cases(64))]
#[test]
fn any_window_braid_consigns_the_projection_exactly(
ops in prop::collection::vec((0u8..3, 0usize..8, 0usize..8), 0..8)
) {
let mut text = Text::new();
for (dot, physical) in [(d(1, 1), 3), (d(1, 2), 2), (d(1, 3), 1)] {
weave(&mut text, dot, locus(Anchor::Origin, rank(physical)));
}
let boundary = Cut::floor_of(text.context());
let mut current = text.clone();
let mut record = Moves::new();
let mut counter = 0u64;
let mut text_deltas = Vec::new();
let mut move_deltas = Vec::new();
for (offset, &(kind, at, to)) in ops.iter().enumerate() {
counter += 1;
let dot = d(2, counter);
let stamp = Kairos::new(100 + u64::try_from(offset).unwrap(), 0, 2, 0u16);
let order = current.store().recension(record.store()).order();
match kind {
0 => {
let anchor = if order.is_empty() {
Anchor::Origin
} else {
Anchor::After(order[at % order.len()].into())
};
let delta = text_delta(dot, locus(anchor, stamp));
current.merge_from(&delta);
text_deltas.push(delta);
}
1 if !order.is_empty() => {
let target = order[at % order.len()];
let mut removal = DotSet::new();
prop_assert!(removal.insert(dot));
let _ = removal.insert(target);
let delta = Dotted::from_context(removal);
current.merge_from(&delta);
text_deltas.push(delta);
}
_ if !order.is_empty() => {
let target = order[at % order.len()];
let anchor = order[to % order.len()];
let anchor = if anchor == target {
Anchor::Origin
} else {
Anchor::After(anchor.into())
};
let delta = movement(dot, target.into(), anchor, stamp);
record.merge_from(&delta);
move_deltas.push(delta);
}
_ => {
let delta = text_delta(dot, locus(Anchor::Origin, stamp));
current.merge_from(&delta);
text_deltas.push(delta);
}
}
}
let window: Vec<(u32, u64)> = (1..=counter).map(|index| (2, index)).collect();
let eager = current.store().recension(record.store());
let frozen = text.store().refound(&Metatheses::new()).unwrap().map().clone();
let mut frozen = frozen;
frozen.bind_cut(&boundary);
let expected: Vec<Dot> = eager
.order()
.into_iter()
.map(|dot| frozen.translate(dot).unwrap())
.collect();
let mut consignments = Vec::new();
for mode in 0..3u8 {
let (adopted, sealed) = seal_mill(1, &boundary, &window);
let mut shadow = EpochStratum::new(&adopted, text.clone(), Moves::new())
.unwrap()
.into_transition()
.shadow;
match mode {
0 => {
for delta in &text_deltas {
shadow.deliver_text(delta).unwrap();
}
for delta in &move_deltas {
shadow.deliver_moves(delta).unwrap();
}
}
1 => {
for delta in move_deltas.iter().rev() {
shadow.deliver_moves(delta).unwrap();
}
for delta in text_deltas.iter().rev() {
shadow.deliver_text(delta).unwrap();
}
}
_ => {
shadow.deliver_text_batch(&text_deltas).unwrap();
shadow.deliver_moves_batch(&move_deltas).unwrap();
}
}
prop_assert_eq!(shadow.projection().order(), expected.as_slice());
consignments.push(shadow.consign(&sealed).unwrap().0);
}
for consignment in &consignments {
prop_assert_eq!(consignment.text().store().order(), expected.clone());
prop_assert_eq!(consignment.moves().store().testimonies().count(), 0);
}
for later in &consignments[1..] {
prop_assert_eq!(
consignments[0].text().store().to_bytes(),
later.text().store().to_bytes()
);
prop_assert_eq!(consignments[0].text().context(), later.text().context());
prop_assert_eq!(consignments[0].moves().context(), later.moves().context());
}
let mut reference = DotSet::new();
let union = current
.context()
.merge(record.context())
.merge(&{
let mut protocol = DotSet::new();
prop_assert!(protocol.insert(d(1, boundary.as_vector().get(1) + 1)));
protocol
});
for dot in union.dots() {
if let Some(new) = frozen.translate(dot) {
let _ = reference.insert(new);
}
}
prop_assert_eq!(consignments[0].text().context(), &reference);
prop_assert_eq!(consignments[0].moves().context(), &reference);
}
}
proptest! {
#[test]
fn projection_agrees_with_eager_judgment_at_every_prefix(
seeds in prop::collection::vec((1u8..=3, 0u8..=3, any::<bool>()), 0..=5)
) {
let mut text = Text::new();
for (dot, physical) in [(d(1, 1), 3), (d(1, 2), 2), (d(1, 3), 1)] {
weave(&mut text, dot, locus(Anchor::Origin, rank(physical)));
}
let frozen = text.store().refound(&Metatheses::new()).unwrap().map().clone();
let mut shadow = open_shadow(text.clone(), Moves::new());
let mut delivered = Moves::new();
for (offset, (target, anchor, before)) in seeds.into_iter().enumerate() {
let anchor = if anchor == 0 {
Anchor::Origin
} else if before {
Anchor::Before(RawDot { station: 1, counter: u64::from(anchor) })
} else {
Anchor::After(RawDot { station: 1, counter: u64::from(anchor) })
};
let delta = movement(
d(2, u64::try_from(offset + 10).unwrap()),
(1, u64::from(target)),
anchor,
rank(u64::try_from(offset + 1).unwrap()),
);
shadow.deliver_moves(&delta).unwrap();
delivered.merge_from(&delta);
let eager = text.store().recension(delivered.store());
let expected: Vec<_> = eager
.order()
.into_iter()
.map(|dot| frozen.translate(dot).unwrap())
.collect();
prop_assert_eq!(shadow.recension().order(), eager.order());
prop_assert_eq!(shadow.recension().refused(), eager.refused());
prop_assert_eq!(shadow.projection().order(), expected);
}
}
}