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
118
119
120
121

use super::{arb_ops, run};
use crate::metis::{Cut, DotSet, DotStore};
use proptest::prelude::*;

proptest! {
    /// `delta_for(peer.context())` converges like the full state.
    #[test]
    fn prop_delta_is_as_good_as_the_full_state(ops in arb_ops()) {
        let (live, _) = run(&ops);
        for state in &live {
            for peer in &live {
                let delta = state.delta_for(peer.context());
                let via_delta = peer.merge(&delta);
                let via_full = peer.merge(state);
                prop_assert_eq!(via_delta, via_full);
            }
        }
    }

    /// A floored delta is full-state-equivalent when the peer floor dominates the cut.
    #[test]
    fn prop_delta_for_since_is_as_good_as_the_full_state(ops in arb_ops()) {
        let (live, _) = run(&ops);
        for state in &live {
            for peer in &live {
                let peer_floor = Cut::floor_of(peer.context());
                for cut in [
                    peer_floor.clone(),
                    Cut::bottom(),
                    peer_floor.meet(&Cut::floor_of(state.context())),
                ] {
                    let delta = state.delta_for_since(&cut);
                    let via_delta = peer.merge(&delta);
                    let via_full = peer.merge(state);
                    prop_assert_eq!(&via_delta, &via_full);
                }
            }
        }
    }

    /// Floored deltas ship the whole survivor store, not the novelty-minimal store.
    #[test]
    fn prop_delta_for_since_ships_the_whole_store(ops in arb_ops()) {
        let (live, _) = run(&ops);
        for state in &live {
            for peer in &live {
                let cut = Cut::floor_of(peer.context());
                let floored = state.delta_for_since(&cut);
                prop_assert_eq!(floored.store(), state.store());
            }
        }
    }

    /// A fresh peer gets the full state.
    #[test]
    fn prop_delta_for_a_fresh_peer_is_the_full_state(ops in arb_ops()) {
        let (live, _) = run(&ops);
        for state in &live {
            let empty = DotSet::new();
            let delta = state.delta_for(&empty);
            prop_assert_eq!(&delta, state);
        }
    }

    /// A current peer gets only removal testimony. (Bottom and support-empty
    /// coincide for this suite's support-only model store; a recording-plane
    /// store ships its plane whole per `novel_to`'s selection law, S190, so
    /// the generic form of this expectation is support-emptiness.)
    #[test]
    fn prop_delta_for_a_current_peer_is_pure_testimony(ops in arb_ops()) {
        let (live, _) = run(&ops);
        for state in &live {
            let delta = state.delta_for(state.context());
            prop_assert!(delta.store().is_bottom());

            let mut held = DotSet::new();
            for dot in state.store().dots() {
                let _ = held.insert(dot);
            }
            let mut superseded = DotSet::new();
            for dot in state.context().difference(&held) {
                let _ = superseded.insert(dot);
            }
            prop_assert_eq!(delta.context(), &superseded);
        }
    }

    /// The witnessed owed read equals the bare read for a support-only store:
    /// the witness licenses recording-plane sub-selection only, and this
    /// suite's model store has no recording plane, so every witness (honest,
    /// over-claiming, or empty) leaves the delta byte-identical. The
    /// recording-carrying law lives with the sequence store's own suite.
    #[test]
    fn prop_witnessed_delta_defaults_to_the_bare_read(ops in arb_ops()) {
        let (live, _) = run(&ops);
        for state in &live {
            for peer in &live {
                let bare = state.delta_for(peer.context());
                for witness in [&DotSet::new(), peer.context(), state.context()] {
                    let witnessed = state.delta_for_witnessed(peer.context(), witness);
                    prop_assert_eq!(&witnessed, &bare);
                }
            }
        }
    }

    /// Delta store dots are exactly outside the peer context.
    #[test]
    fn prop_delta_store_dots_are_uncovered_by_the_peer(ops in arb_ops()) {
        let (live, _) = run(&ops);
        for state in &live {
            for peer in &live {
                let delta = state.delta_for(peer.context());
                let peer_context = peer.context();
                for dot in delta.store().dots() {
                    prop_assert!(!peer_context.contains(dot));
                }
            }
        }
    }
}