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
62
63
64
65

use super::super::super::support::arb_vv;
use proptest::prelude::*;

proptest! {
    /// Merge is a semilattice join: commutative, associative, idempotent.
    #[test]
    fn prop_merge_commutative_associative_idempotent(
        a in arb_vv(), b in arb_vv(), c in arb_vv(),
    ) {
        prop_assert_eq!(a.merge(&b), b.merge(&a));
        prop_assert_eq!(a.merge(&b).merge(&c), a.merge(&b.merge(&c)));
        prop_assert_eq!(a.merge(&a), a);
    }

    /// Merge is the least upper bound, and it is exactly the pointwise maximum.
    #[test]
    fn prop_merge_is_least_upper_bound(a in arb_vv(), b in arb_vv()) {
        let m = a.merge(&b);
        prop_assert!(a <= m);
        prop_assert!(b <= m);
        // Pin the join as pointwise max over the generation domain and beyond.
        for station in 0u32..8 {
            prop_assert_eq!(m.get(station), a.get(station).max(b.get(station)));
        }
    }

    /// Meet is a semilattice meet: commutative, associative, idempotent.
    #[test]
    fn prop_meet_commutative_associative_idempotent(
        a in arb_vv(), b in arb_vv(), c in arb_vv(),
    ) {
        prop_assert_eq!(a.meet(&b), b.meet(&a));
        prop_assert_eq!(a.meet(&b).meet(&c), a.meet(&b.meet(&c)));
        prop_assert_eq!(a.meet(&a), a);
    }

    /// Meet is the greatest lower bound, and it is exactly the pointwise minimum.
    #[test]
    fn prop_meet_is_greatest_lower_bound(
        a in arb_vv(), b in arb_vv(), c in arb_vv(),
    ) {
        let m = a.meet(&b);
        prop_assert!(m <= a);
        prop_assert!(m <= b);
        // Greatest: a vector is a common lower bound iff it lies below the meet.
        prop_assert_eq!(c <= a && c <= b, c <= m);
        // Pin the meet as pointwise min over the generation domain and beyond.
        for station in 0u32..8 {
            prop_assert_eq!(m.get(station), a.get(station).min(b.get(station)));
        }
    }

    /// Join and meet absorb each other and distribute both ways: the vector
    /// order is a distributive lattice, now exercised in code rather than
    /// inherited from the ambient mathematics.
    #[test]
    fn prop_join_meet_absorption_and_distributivity(
        a in arb_vv(), b in arb_vv(), c in arb_vv(),
    ) {
        prop_assert_eq!(&a.meet(&a.merge(&b)), &a);
        prop_assert_eq!(&a.merge(&a.meet(&b)), &a);
        prop_assert_eq!(a.meet(&b.merge(&c)), a.meet(&b).merge(&a.meet(&c)));
        prop_assert_eq!(a.merge(&b.meet(&c)), a.merge(&b).meet(&a.merge(&c)));
    }
}