minerva 0.2.0

Causal ordering for distributed systems
extern crate alloc;

use alloc::vec::Vec;

use crate::metis::{Dot, DotStore};
use proptest::prelude::*;

use super::super::{REPLICAS, Seq, arb_ops_with_paste, reference_order, run};

proptest! {
    /// After any collaborative-edit history, both folds converge and the
    /// fold's document order equals the independent reference oracle.
    #[test]
    fn prop_replicas_converge_to_the_order_oracle(ops in arb_ops_with_paste()) {
        let (live, record) = run(&ops);
        let forward = live.iter().fold(Seq::new(), |acc, r| acc.merge(r));
        let backward = live.iter().rev().fold(Seq::new(), |acc, r| acc.merge(r));

        prop_assert_eq!(&forward, &backward);
        for r in &live {
            prop_assert_eq!(&forward.merge(r), &forward);
        }

        let expected = reference_order(&record);
        let got = forward.store().order();
        prop_assert_eq!(got, expected);
    }

    /// The in-place sequence fold agrees with the pure merge on every
    /// run-reached state: the Rhapsody `causal_merge_from` override (the
    /// incremental skeleton and child-index insert plus the in-place survivor
    /// fold, S182) is `merge` in cost clothing. Equality covers the child
    /// index derivationally: `order()` walks it, and the states compare equal
    /// on the carried coordinates, so the cached order is asserted equal too.
    #[test]
    fn prop_rhapsody_merge_from_agrees_with_merge(ops in arb_ops_with_paste()) {
        let (live, _) = run(&ops);
        for a in &live {
            for b in &live {
                let mut folded = a.clone();
                folded.merge_from(b);
                prop_assert_eq!(&folded, &a.merge(b));
                prop_assert_eq!(folded.store().order(), a.merge(b).store().order());
            }
        }
    }

    /// The document order is a function of recorded loci, not merge history.
    #[test]
    fn prop_order_is_fold_order_independent(
        ops in arb_ops_with_paste(),
        extra in prop::collection::vec(0usize..REPLICAS, 0..REPLICAS),
        shuffle in Just((0..REPLICAS).collect::<Vec<usize>>()).prop_shuffle(),
    ) {
        let (live, _) = run(&ops);
        let fold = |seq: &[usize]| -> Vec<Dot> {
            let mut acc = Seq::new();
            for &i in seq {
                acc = acc.merge(&live[i]);
            }
            acc.store().order()
        };
        let mut permuted = shuffle;
        permuted.extend(extra);
        let a = fold(&(0..REPLICAS).collect::<Vec<_>>());
        let b = fold(&permuted);
        prop_assert_eq!(a, b);
    }

    /// The grow-only skeleton holds every dot ever woven.
    #[test]
    fn prop_skeleton_is_grow_only(ops in arb_ops_with_paste()) {
        let (live, record) = run(&ops);
        let forward = live.iter().fold(Seq::new(), |acc, r| acc.merge(r));
        for &dot in record.woven.keys() {
            prop_assert!(forward.store().locus(dot).is_some());
        }
        prop_assert_eq!(forward.store().skeleton_len(), record.woven.len());
    }

    /// The visible set is exactly the woven-and-never-deleted dots.
    #[test]
    fn prop_visible_is_woven_minus_expelled(ops in arb_ops_with_paste()) {
        let (live, record) = run(&ops);
        let forward = live.iter().fold(Seq::new(), |acc, r| acc.merge(r));
        let mut want: Vec<Dot> = record
            .woven
            .keys()
            .copied()
            .filter(|dot| !record.expelled.contains(dot))
            .collect();
        want.sort_unstable();
        let mut got: Vec<Dot> = forward.store().dots().collect();
        got.sort_unstable();
        prop_assert_eq!(got, want);
    }
}