minerva 0.2.0

//! Generated agreement between maintained collation and eager replay.

use proptest::prelude::*;

use super::*;

const REPLICAS: usize = 3;

/// The replay operations plus move-only gossip, which can outrun a weave.
#[derive(Clone, Debug)]
enum Op {
    Insert {
        replica: usize,
        caret_pick: usize,
    },
    Delete {
        replica: usize,
        victim_pick: usize,
    },
    Move {
        replica: usize,
        target_pick: usize,
        dest_pick: usize,
        before: bool,
    },
    Undo {
        replica: usize,
        testimony_pick: usize,
    },
    Gossip {
        from: usize,
        to: usize,
    },
    GossipMoves {
        from: usize,
        to: usize,
    },
}

fn arb_ops() -> impl Strategy<Value = Vec<Op>> {
    let op = prop_oneof![
        3 => (0..REPLICAS, 0usize..8)
            .prop_map(|(replica, caret_pick)| Op::Insert { replica, caret_pick }),
        1 => (0..REPLICAS, 0usize..8)
            .prop_map(|(replica, victim_pick)| Op::Delete { replica, victim_pick }),
        3 => (0..REPLICAS, 0usize..8, 0usize..8, any::<bool>()).prop_map(
            |(replica, target_pick, dest_pick, before)| Op::Move {
                replica,
                target_pick,
                dest_pick,
                before,
            }
        ),
        1 => (0..REPLICAS, 0usize..8)
            .prop_map(|(replica, testimony_pick)| Op::Undo { replica, testimony_pick }),
        2 => (0..REPLICAS, 0..REPLICAS).prop_map(|(from, to)| Op::Gossip { from, to }),
        2 => (0..REPLICAS, 0..REPLICAS).prop_map(|(from, to)| Op::GossipMoves { from, to }),
    ];
    prop::collection::vec(op, 0..32)
}

fn gossip_text(fleet: &mut [(Text, Moves)], from: usize, to: usize) {
    let delta = fleet[from].0.owed_to(fleet[to].0.state().context());
    let sender = u32::try_from(from + 1).unwrap();
    let _ = fleet[to].0.absorb(sender, &delta);
}

fn gossip_moves(fleet: &mut [(Text, Moves)], from: usize, to: usize) {
    let delta = fleet[from].1.owed_to(fleet[to].1.state().context());
    let sender = u32::try_from(from + 1).unwrap();
    let _ = fleet[to].1.absorb(sender, &delta);
}

proptest! {
    /// Every maintained view agrees with eager replay after each operation.
    #[test]
    fn prop_collation_agrees_with_the_eager_replay(ops in arb_ops()) {
        let mut fleet: Vec<(Text, Moves)> = (0..REPLICAS)
            .map(|i| {
                let station = u32::try_from(i + 1).unwrap();
                (Text::new(station), Moves::new(station))
            })
            .collect();
        let clocks: Vec<_> = (0..REPLICAS)
            .map(|i| clock(u32::try_from(i + 1).unwrap()))
            .collect();
        // Starting empty forces the first collation through incremental paths.
        let mut maintained: Vec<crate::metis::Recension> = (0..REPLICAS)
            .map(|_| Rhapsody::new().recension(&Metatheses::new()))
            .collect();

        for op in &ops {
            match *op {
                Op::Insert { replica, caret_pick } => {
                    let visible = fleet[replica].0.state().store().order();
                    let caret = if visible.is_empty() {
                        None
                    } else {
                        Some(visible[caret_pick % visible.len()].into())
                    };
                    let _ = type_after(&mut fleet[replica].0, &clocks[replica], caret);
                }
                Op::Delete { replica, victim_pick } => {
                    let visible = fleet[replica].0.state().store().order();
                    if visible.is_empty() {
                        continue;
                    }
                    let victim = visible[victim_pick % visible.len()];
                    let mut gone = DotSet::new();
                    let _ = gone.insert(victim);
                    let _ = fleet[replica].0.retract(gone);
                }
                Op::Move { replica, target_pick, dest_pick, before } => {
                    let woven: Vec<Dot> =
                        fleet[replica].0.state().store().woven().dots().collect();
                    if woven.len() < 2 {
                        continue;
                    }
                    let target = woven[target_pick % woven.len()];
                    let dest = woven[dest_pick % woven.len()];
                    let anchor = if before {
                        Anchor::Before(dest.into())
                    } else {
                        Anchor::After(dest.into())
                    };
                    let to = locus_at(&clocks[replica], anchor);
                    let _ = move_to(&mut fleet[replica].1, target.into(), to);
                }
                Op::Undo { replica, testimony_pick } => {
                    let held: Vec<Dot> = fleet[replica]
                        .1
                        .state()
                        .store()
                        .iter()
                        .map(|(dot, _)| dot)
                        .collect();
                    if held.is_empty() {
                        continue;
                    }
                    let victim = held[testimony_pick % held.len()];
                    let mut undo = DotSet::new();
                    let _ = undo.insert(victim);
                    let _ = fleet[replica].1.retract(undo);
                }
                Op::Gossip { from, to } => {
                    if from != to {
                        gossip_text(&mut fleet, from, to);
                        gossip_moves(&mut fleet, from, to);
                    }
                }
                Op::GossipMoves { from, to } => {
                    if from != to {
                        gossip_moves(&mut fleet, from, to);
                    }
                }
            }
            for (view, (text, moves)) in maintained.iter_mut().zip(&fleet) {
                view.collate(text.state().store(), moves.state().store());
                let eager = text.state().store().recension(moves.state().store());
                view.check_collation(&eager);
            }
        }
        for (view, (text, moves)) in maintained.iter_mut().zip(&fleet) {
            let replays = view.collation_replays();
            let rebuilds = view.collation_rebuilds();
            view.collate(text.state().store(), moves.state().store());
            prop_assert_eq!(view.collation_replays(), replays);
            prop_assert_eq!(view.collation_rebuilds(), rebuilds);
        }
    }
}