minerva 0.2.0

Causal ordering for distributed systems
use super::{arb_notes, model_common, roster};
use crate::metis::{Purview, Received};
use proptest::prelude::*;

proptest! {
    /// `common` equals the naive model intersection of all rows, and never
    /// regresses under further evidence.
    #[test]
    fn prop_common_is_the_intersection_and_never_regresses(notes in arb_notes()) {
        let roster = roster();
        let mut purview = Purview::new(roster.iter().copied());
        let mut last = purview.common();
        for (peer, seen) in &notes {
            purview.note(&Received::trust(*peer, seen.clone())).unwrap();
            let common = purview.common();
            let model = model_common(&purview, &roster);
            prop_assert_eq!(&common, &model);
            // Never regresses: the new common is its own merge with the prior.
            let rejoin = common.merge(&last);
            prop_assert_eq!(&rejoin, &common);
            last = common;
        }
    }

    /// `common_floor` is exactly `common().floor()`.
    #[test]
    fn prop_common_floor_is_the_floor_of_common(notes in arb_notes()) {
        let mut purview = Purview::new(roster());
        for (peer, seen) in &notes {
            purview.note(&Received::trust(*peer, seen.clone())).unwrap();
        }
        let floor = purview.common().floor();
        prop_assert_eq!(purview.common_floor(), floor);
    }
}