minerva 0.2.0

Causal ordering for distributed systems
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

extern crate alloc;

use alloc::collections::BTreeMap;

use super::{arb_notes, roster};
use crate::metis::{DotSet, Purview, Received};
use proptest::prelude::*;

proptest! {
    /// Rows are evidence-order-invariant: any permutation and duplication of a
    /// fixed multiset of `note` calls yields the identical tracker.
    #[test]
    fn prop_rows_are_evidence_order_invariant(
        (notes, permuted) in arb_notes()
            .prop_flat_map(|n| (Just(n.clone()), Just(n).prop_shuffle())),
    ) {
        let mut a = Purview::new(roster());
        for (peer, seen) in &notes {
            a.note(&Received::trust(*peer, seen.clone())).unwrap();
        }
        // Duplicate every note in the permuted stream: duplication is absorbed.
        let mut b = Purview::new(roster());
        for (peer, seen) in &permuted {
            b.note(&Received::trust(*peer, seen.clone())).unwrap();
            b.note(&Received::trust(*peer, seen.clone())).unwrap();
        }
        prop_assert_eq!(&a, &b);
    }

    /// Rows are monotone: no row ever regresses across a note, whatever its
    /// staleness.
    #[test]
    fn prop_rows_never_regress(notes in arb_notes()) {
        let roster = roster();
        let mut purview = Purview::new(roster.iter().copied());
        let mut last: BTreeMap<u32, DotSet> =
            roster.iter().map(|&p| (p, DotSet::new())).collect();
        for (peer, seen) in &notes {
            purview.note(&Received::trust(*peer, seen.clone())).unwrap();
            for &p in &roster {
                let now = purview.of(p).unwrap();
                let before = &last[&p];
                // Monotone growth: the row is its own merge with the prior row.
                let rejoin = now.merge(before);
                prop_assert_eq!(&rejoin, now);
                let _ = last.insert(p, now.clone());
            }
        }
    }
}