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
51
52
53
54
55
56
57
58
59
60
61

extern crate alloc;

use alloc::collections::BTreeSet;

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

use super::{arb_seed, covered, value_for};

proptest! {
    /// `novel_to` selects exactly the held dots the peer context has not seen,
    /// with content preserved.
    #[test]
    fn prop_novel_to_selects_the_unseen_dots(a in arb_seed(), b in arb_seed()) {
        let ca = covered(&a);
        let cb = covered(&b);
        let novel = ca.store().novel_to(cb.context());
        let held: BTreeSet<Dot> = ca.store().dots().collect();
        let want: BTreeSet<Dot> = held
            .iter()
            .copied()
            .filter(|&dot| !cb.context().contains(dot))
            .collect();
        let got: BTreeSet<Dot> = novel.dots().collect();
        prop_assert_eq!(&got, &want);
        for dot in novel.dots() {
            let value = novel.get(dot).expect("novel carries its content");
            prop_assert_eq!(value, &value_for(dot.station(), dot.counter()));
        }
    }

    /// Restriction is fiber selection and commutes with causal merge under
    /// restricted contexts.
    #[test]
    fn prop_restrict_commutes_with_merge(
        a in arb_seed(), b in arb_seed(),
        roster in prop::collection::vec(0u32..4, 0..4),
    ) {
        let ca = covered(&a);
        let cb = covered(&b);

        let kept = ca.store().restrict(roster.iter().copied());
        let roster_set: BTreeSet<u32> = roster.iter().copied().collect();
        let want: BTreeSet<Dot> = ca
            .store()
            .dots()
            .filter(|dot| roster_set.contains(&dot.station()))
            .collect();
        let got: BTreeSet<Dot> = kept.dots().collect();
        prop_assert_eq!(&got, &want);

        let merged = ca.store().causal_merge(ca.context(), cb.store(), cb.context());
        let restrict_then_merge = ca.store().restrict(roster.iter().copied()).causal_merge(
            &ca.context().restrict(roster.iter().copied()),
            &cb.store().restrict(roster.iter().copied()),
            &cb.context().restrict(roster.iter().copied()),
        );
        let lhs = merged.restrict(roster.iter().copied());
        prop_assert_eq!(lhs, restrict_then_merge);
    }
}