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

use crate::metis::{Cut, with_scope};
use proptest::prelude::*;

use super::{arb_dots, arb_roster, have};

proptest! {
    /// Scoped have-set folds commute with unbranded restriction.
    #[test]
    fn prop_scoped_dot_folds_commute_with_restriction(
        a in arb_dots(), b in arb_dots(), r in arb_roster(),
    ) {
        let (sa, sb) = (have(&a), have(&b));
        let expected_merge = sa.merge(&sb).restrict(r.iter().copied());
        let expected_intersect = sa.intersect(&sb).restrict(r.iter().copied());
        let expected_floor = sa.floor().restrict(r.iter().copied());
        let (merged, intersected, floored) = with_scope(r.iter().copied(), |scope| {
            let ra = scope.restrict_dots(&sa);
            let rb = scope.restrict_dots(&sb);
            (
                ra.merge(&rb).forget(),
                ra.intersect(&rb).forget(),
                ra.floor().forget(),
            )
        });
        prop_assert_eq!(merged, expected_merge);
        prop_assert_eq!(intersected, expected_intersect);
        prop_assert_eq!(floored, expected_floor);
    }

    /// `floor_cut` agrees with forget-then-floor_of, so the witness travels
    /// without dropping the brand mid-flight.
    #[test]
    fn prop_floor_cut_agrees_with_forget_then_floor_of(
        dots in arb_dots(), r in arb_roster(),
    ) {
        let set = have(&dots);
        let (branded, forgotten) = with_scope(r.iter().copied(), |scope| {
            let sd = scope.restrict_dots(&set);
            (sd.floor_cut().forget(), sd.forget())
        });
        prop_assert_eq!(&branded, &Cut::floor_of(&forgotten));
        prop_assert_eq!(
            branded.into_vector(),
            set.floor().restrict(r.iter().copied()),
        );
    }
}