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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98

extern crate alloc;

use alloc::collections::BTreeSet;
use alloc::vec::Vec;

use super::super::super::support::{arb_vv, dot};
use super::{arb_dots, arb_subroster, have, model};
use crate::metis::{Dot, DotSet};
use proptest::prelude::*;

proptest! {
    /// Difference enumerates exactly the owed dots in ascending order.
    #[test]
    fn prop_difference_is_the_exact_owed_set(a in arb_dots(), b in arb_dots()) {
        let (sa, sb) = (have(&a), have(&b));
        let owed: Vec<Dot> = sa.difference(&sb).collect();
        for pair in owed.windows(2) {
            prop_assert!(pair[0] < pair[1]);
        }
        let yielded: BTreeSet<Dot> = owed.iter().copied().collect();
        prop_assert_eq!(yielded.len(), owed.len());
        let expected: BTreeSet<Dot> =
            model(&a).difference(&model(&b)).copied().collect();
        prop_assert_eq!(yielded, expected);
    }

    /// Repaying the debt yields exactly the union.
    #[test]
    fn prop_difference_repays_to_the_union(a in arb_dots(), b in arb_dots()) {
        let (sa, sb) = (have(&a), have(&b));
        let mut repaid = sb.clone();
        for owed in sa.difference(&sb) {
            prop_assert!(repaid.insert(owed));
        }
        prop_assert_eq!(repaid, sa.merge(&sb));
        let nothing_owed = sa.difference(&sb).next().is_none();
        prop_assert_eq!(nothing_owed, model(&a).is_subset(&model(&b)));
    }

    /// Whole-set coverage agrees with the empty-difference law.
    #[test]
    fn prop_covers_is_empty_difference(a in arb_dots(), b in arb_dots()) {
        let (sa, sb) = (have(&a), have(&b));
        prop_assert_eq!(sa.covers(&sb), sb.difference(&sa).next().is_none());
        prop_assert_eq!(sb.covers(&sa), sa.difference(&sb).next().is_none());
        prop_assert!(sa.covers(&sa));
        prop_assert_eq!(sa.covers(&sb), model(&b).is_subset(&model(&a)));
        let union = sa.merge(&sb);
        prop_assert!(union.covers(&sa));
        prop_assert!(union.covers(&sb));
    }

    /// Holes and parked exceptions are both difference reads.
    #[test]
    fn prop_holes_and_exceptions_are_difference_reads(dots in arb_dots()) {
        let set = have(&dots);
        let closure = DotSet::from_cut(&set.high_water());
        let via_difference: Vec<Dot> = closure.difference(&set).collect();
        let direct: Vec<Dot> = set.holes().collect();
        prop_assert_eq!(via_difference, direct);
        let interior = DotSet::from_cut(&set.floor());
        prop_assert_eq!(set.difference(&interior).count(), set.exceptions_len());
    }

    /// Between two genuine cuts, owed dots are exactly the vector residual spans.
    #[test]
    fn prop_cut_difference_enumerates_the_residual_spans(
        v in arb_vv(), w in arb_vv(),
    ) {
        let (dv, dw) = (DotSet::from_cut(&v), DotSet::from_cut(&w));
        let owed: Vec<Dot> = dv.difference(&dw).collect();
        let mut expected = Vec::new();
        for (station, claim) in &v.difference(&w) {
            for counter in w.get(station).saturating_add(1)..=claim {
                expected.push(dot(station, counter));
            }
        }
        prop_assert_eq!(owed, expected);
    }

    /// Difference commutes exactly with restriction.
    #[test]
    fn prop_difference_commutes_with_restriction(
        a in arb_dots(), b in arb_dots(), roster in arb_subroster(),
    ) {
        let (sa, sb) = (have(&a), have(&b));
        let (ra, rb) = (
            sa.restrict(roster.iter().copied()),
            sb.restrict(roster.iter().copied()),
        );
        let restricted: Vec<Dot> = ra.difference(&rb).collect();
        let filtered: Vec<Dot> = sa
            .difference(&sb)
            .filter(|owed| roster.contains(&owed.station()))
            .collect();
        prop_assert_eq!(restricted, filtered);
    }
}