extern crate alloc;
use super::{Doc, Op, SCRIBES, arb_ops, observed};
use crate::metis::{Composer, DotMap, DotSet, Dotted};
use alloc::vec::Vec;
use proptest::prelude::*;
proptest! {
#[test]
fn prop_delta_exchange_converges_like_full_states(ops in arb_ops()) {
let mut composers: Vec<Composer<Doc>> = (0..SCRIBES)
.map(|i| Composer::new(u32::try_from(i).unwrap()))
.collect();
let mut states: Vec<Dotted<Doc>> = (0..SCRIBES).map(|_| Dotted::new()).collect();
for op in &ops {
match *op {
Op::Add { composer, key } => {
let _ = composers[composer].compose(move |assigned| {
let mut held = DotSet::new();
let _ = held.insert(assigned);
(DotMap::singleton(key, held), DotSet::new())
});
let station = u32::try_from(composer).unwrap();
let assigned = states[composer].next_dot(station);
let mut held = DotSet::new();
let _ = held.insert(assigned);
let delta = Dotted::from_store(DotMap::singleton(key, held));
states[composer] = states[composer].merge(&delta);
}
Op::Remove { composer, key } => {
let seen = observed(composers[composer].state(), key);
let _ = composers[composer].retract(seen);
let obs = observed(&states[composer], key);
states[composer] = states[composer].merge(&Dotted::from_context(obs));
}
Op::Gossip { from, to } => {
let delta = composers[from].owed_to(composers[to].state().context());
let _ = composers[to].absorb(u32::try_from(from).unwrap(), &delta);
let full = states[from].clone();
states[to] = states[to].merge(&full);
}
}
}
let full_fold = states.iter().fold(Dotted::new(), |acc, s| acc.merge(s));
let snapshots: Vec<Dotted<Doc>> = composers.iter().map(|s| s.state().clone()).collect();
let mut converged = composers;
for (to, composer) in converged.iter_mut().enumerate() {
for (from, snapshot) in snapshots.iter().enumerate() {
if from == to {
continue;
}
let delta = Composer::adopt(u32::try_from(from).unwrap(), snapshot.clone())
.owed_to(composer.state().context());
let _ = composer.absorb(u32::try_from(from).unwrap(), &delta);
}
}
for composer in &converged {
prop_assert_eq!(composer.state(), &full_fold);
}
}
}