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

extern crate alloc;

use alloc::vec::Vec;

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

proptest! {
    /// Restriction is fiber selection and remains canonical.
    #[test]
    fn prop_restrict_is_the_fiber_selection(
        dots in arb_dots(), roster in arb_subroster(),
    ) {
        let set = have(&dots);
        let restricted = set.restrict(roster.iter().copied());
        // The sweep starts at counter one: zero is no dot, so the arm that
        // once read `contains(station, 0)` is unrepresentable (ruling R-91).
        for station in 0u32..4 {
            for counter in 1u64..13 {
                prop_assert_eq!(
                    restricted.contains(dot(station, counter)),
                    roster.contains(&station) && set.contains(dot(station, counter))
                );
            }
        }
        let kept: Vec<(u32, u64)> = dots
            .iter()
            .copied()
            .filter(|&(station, _)| roster.contains(&station))
            .collect();
        prop_assert_eq!(restricted, have(&kept));
    }

    /// Base change is exact against every read and fold on the type.
    #[test]
    fn prop_restrict_commutes_with_every_read_and_fold(
        a in arb_dots(), b in arb_dots(), roster in arb_subroster(),
    ) {
        let (sa, sb) = (have(&a), have(&b));
        let restricted = sa.restrict(roster.iter().copied());
        prop_assert_eq!(
            sa.merge(&sb).restrict(roster.iter().copied()),
            restricted.merge(&sb.restrict(roster.iter().copied()))
        );
        prop_assert_eq!(restricted.floor(), sa.floor().restrict(roster.iter().copied()));
        prop_assert_eq!(
            restricted.high_water(),
            sa.high_water().restrict(roster.iter().copied())
        );
        let restricted_holes: Vec<Dot> = restricted.holes().collect();
        let filtered_holes: Vec<Dot> = sa
            .holes()
            .filter(|hole| roster.contains(&hole.station()))
            .collect();
        prop_assert_eq!(restricted_holes, filtered_holes);
        prop_assert_eq!(
            DotSet::from_cut(&sa.floor()).restrict(roster.iter().copied()),
            DotSet::from_cut(&sa.floor().restrict(roster.iter().copied()))
        );
    }
}