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
115
116
117

extern crate alloc;

use alloc::vec::Vec;

use super::super::super::support::arb_vv;
use super::arb_roster;
use crate::metis::VersionVector;
use proptest::prelude::*;

proptest! {
    /// Restriction is the base change along a sub-roster inclusion, and it is
    /// functorial: the identity on any roster covering the support, bottom on
    /// the empty roster, idempotent, and composing by roster intersection.
    #[test]
    fn prop_restrict_is_functorial(
        a in arb_vv(), r in arb_roster(), s in arb_roster(),
    ) {
        // 0..8 covers the 0..6 generation domain, so it covers the support.
        prop_assert_eq!(&a.restrict(0u32..8), &a);
        prop_assert_eq!(a.restrict(core::iter::empty::<u32>()), VersionVector::new());
        let ra = a.restrict(r.iter().copied());
        prop_assert_eq!(&ra.restrict(r.iter().copied()), &ra);
        let intersection: Vec<u32> =
            r.iter().copied().filter(|station| s.contains(station)).collect();
        prop_assert_eq!(
            a.restrict(r.iter().copied()).restrict(s.iter().copied()),
            a.restrict(intersection)
        );
    }

    /// Restriction is a bounded-lattice homomorphism: it commutes with the
    /// join and the meet and preserves the order. And the witness travels one
    /// way: concurrent restrictions reflect to concurrent originals (the
    /// converse, order created by restriction, is pinned as an example test).
    #[test]
    fn prop_restrict_is_a_lattice_homomorphism_and_reflects_concurrency(
        a in arb_vv(), b in arb_vv(), r in arb_roster(),
    ) {
        let ra = a.restrict(r.iter().copied());
        let rb = b.restrict(r.iter().copied());
        prop_assert_eq!(a.merge(&b).restrict(r.iter().copied()), ra.merge(&rb));
        prop_assert_eq!(a.meet(&b).restrict(r.iter().copied()), ra.meet(&rb));
        if a <= b {
            prop_assert!(ra <= rb);
        }
        if ra.concurrent(&rb) {
            prop_assert!(a.concurrent(&b));
        }
    }

    /// The sheaf condition: local sections cut from one vector always re-glue,
    /// over any overlap inside both rosters, to the restriction over the union
    /// of the rosters.
    #[test]
    fn prop_sections_of_one_vector_glue_back(
        v in arb_vv(), r in arb_roster(), s in arb_roster(),
    ) {
        let vr = v.restrict(r.iter().copied());
        let vs = v.restrict(s.iter().copied());
        let overlap: Vec<u32> =
            r.iter().copied().filter(|station| s.contains(station)).collect();
        let glued = v_glued(&vr, &vs, &overlap)?;
        let union = r.iter().copied().chain(s.iter().copied());
        prop_assert_eq!(glued, v.restrict(union));
    }

    /// The glue is exact where the merge is lax: an empty overlap degenerates
    /// to the merge, agreement on the overlap glues to the merge, and a
    /// disagreement refuses with the first witness in overlap order,
    /// symmetrically in the two sections.
    #[test]
    fn prop_glue_refuses_disagreement_with_the_first_witness(
        a in arb_vv(), b in arb_vv(),
    ) {
        prop_assert_eq!(
            a.try_glue(&b, core::iter::empty::<u32>()),
            Ok(a.merge(&b))
        );
        // Claim authority over the whole generation domain on both sides.
        match a.try_glue(&b, 0u32..8) {
            Ok(glued) => {
                prop_assert_eq!(&glued, &a.merge(&b));
                for station in 0u32..8 {
                    prop_assert_eq!(a.get(station), b.get(station));
                }
            }
            Err(witness) => {
                prop_assert_eq!(witness.left, a.get(witness.station));
                prop_assert_eq!(witness.right, b.get(witness.station));
                prop_assert_ne!(witness.left, witness.right);
                // First disagreement in overlap order: everything below agrees.
                for station in 0..witness.station {
                    prop_assert_eq!(a.get(station), b.get(station));
                }
                let mirrored = b.try_glue(&a, 0u32..8).unwrap_err();
                prop_assert_eq!(mirrored.station, witness.station);
                prop_assert_eq!(mirrored.left, witness.right);
                prop_assert_eq!(mirrored.right, witness.left);
            }
        }
    }
}

/// Unwraps a glue the property expects to succeed, converting a refusal into a
/// test failure with the witness in the message.
fn v_glued(
    left: &VersionVector,
    right: &VersionVector,
    overlap: &[u32],
) -> Result<VersionVector, TestCaseError> {
    left.try_glue(right, overlap.iter().copied())
        .map_err(|witness| {
            TestCaseError::fail(alloc::format!(
                "sections of one vector must glue, got {witness:?}"
            ))
        })
}