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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114

extern crate alloc;

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

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

proptest! {
    /// The floor is the greatest genuine cut inside the have-set.
    #[test]
    fn prop_floor_is_the_greatest_contained_cut(dots in arb_dots()) {
        let set = have(&dots);
        let floor = set.floor();
        for station in 0u32..4 {
            let prefix = floor.get(station);
            for counter in 1..=prefix {
                prop_assert!(set.contains(dot(station, counter)));
            }
            prop_assert!(!set.contains(dot(station, prefix.saturating_add(1))));
        }
    }

    /// The closure commutes with joins while the interior is only lax.
    #[test]
    fn prop_high_water_is_a_join_homomorphism_and_floor_is_lax(
        a in arb_dots(), b in arb_dots(),
    ) {
        let (sa, sb) = (have(&a), have(&b));
        let union = sa.merge(&sb);
        prop_assert_eq!(
            union.high_water(),
            sa.high_water().merge(&sb.high_water())
        );
        let joined_floors = sa.floor().merge(&sb.floor());
        prop_assert!(joined_floors <= union.floor());
    }

    /// The holes are exactly the dots below high water that are not held.
    #[test]
    fn prop_holes_are_exactly_the_missing_dots(dots in arb_dots()) {
        let set = have(&dots);
        let high_water = set.high_water();
        let holes: BTreeSet<Dot> = set.holes().collect();
        let mut expected = BTreeSet::new();
        for station in 0u32..4 {
            for counter in 1..=high_water.get(station) {
                if !set.contains(dot(station, counter)) {
                    let _ = expected.insert(dot(station, counter));
                }
            }
        }
        prop_assert_eq!(holes, expected);
    }

    /// The per-station hole read equals whole-set holes filtered to that station.
    #[test]
    fn prop_holes_for_is_the_whole_set_filtered(dots in arb_dots()) {
        let set = have(&dots);
        for station in 0u32..6 {
            let per_station: Vec<u64> = set.holes_for(station).collect();
            let filtered: Vec<u64> = set
                .holes()
                .filter(|hole| hole.station() == station)
                .map(Dot::counter)
                .collect();
            prop_assert_eq!(per_station, filtered);
        }
    }

    /// The hole count is the whole-set holes counted.
    #[test]
    fn prop_hole_count_equals_holes_counted(dots in arb_dots()) {
        let set = have(&dots);
        let counted = u64::try_from(set.holes().count()).unwrap();
        prop_assert_eq!(set.hole_count(), counted);
    }

    /// The two bracketing cuts never regress under insertion.
    #[test]
    fn prop_floor_and_high_water_bracket_and_never_regress(dots in arb_dots()) {
        let mut set = DotSet::new();
        let mut last_floor = set.floor();
        let mut last_high = set.high_water();
        for pair in dots {
            // A drawn zero counter is no dot and cannot be offered: the same
            // no-op the door's refusal used to give (ruling R-91).
            if let Ok(dot) = Dot::try_from(pair) {
                let _ = set.insert(dot);
            }
            let floor = set.floor();
            let high = set.high_water();
            prop_assert!(last_floor <= floor);
            prop_assert!(last_high <= high);
            prop_assert!(floor <= high);
            last_floor = floor;
            last_high = high;
        }
    }

    /// A witnessed cut embeds losslessly.
    #[test]
    fn prop_from_witnessed_embeds_the_cut(cut in arb_vv()) {
        let witness = Cut::floor_of(&DotSet::from_cut(&cut));
        prop_assert_eq!(witness.as_vector(), &cut);
        let set = DotSet::from_witnessed(&witness);
        prop_assert_eq!(set.floor(), cut);
        prop_assert_eq!(set.high_water(), set.floor());
        prop_assert_eq!(set.holes().count(), 0);
        prop_assert_eq!(set.exceptions_len(), 0);
    }
}