minerva 0.2.0

Causal ordering for distributed systems
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);
        }
    }
}