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

extern crate alloc;

use super::{Doc, Op, SCRIBES, arb_ops, observed};
use crate::metis::{Composer, DotMap, DotSet, Dotted};
use alloc::vec::Vec;
use proptest::prelude::*;

proptest! {
    #[test]
    fn prop_scribe_matches_the_manual_flow(ops in arb_ops()) {
        let mut composers: Vec<Composer<Doc>> = (0..SCRIBES)
            .map(|i| Composer::new(u32::try_from(i).unwrap()))
            .collect();
        let mut manual: Vec<Dotted<Doc>> = (0..SCRIBES).map(|_| Dotted::new()).collect();

        for op in &ops {
            match *op {
                Op::Add { composer, key } => {
                    let (via_dot, via_scribe) = composers[composer].compose(move |assigned| {
                        let mut held = DotSet::new();
                        let _ = held.insert(assigned);
                        (DotMap::singleton(key, held), DotSet::new())
                    });

                    let station = u32::try_from(composer).unwrap();
                    let assigned = manual[composer].next_dot(station);
                    let mut held = DotSet::new();
                    let _ = held.insert(assigned);
                    let by_hand = Dotted::from_store(DotMap::singleton(key, held));
                    manual[composer] = manual[composer].merge(&by_hand);

                    prop_assert_eq!(&via_scribe, &by_hand);
                    prop_assert_eq!(via_dot, assigned);
                    prop_assert_eq!(composers[composer].state(), &manual[composer]);
                }
                Op::Remove { composer, key } => {
                    let seen = observed(composers[composer].state(), key);
                    let via_scribe = composers[composer].retract(seen);
                    let obs = observed(&manual[composer], key);
                    let by_hand = Dotted::from_context(obs);
                    manual[composer] = manual[composer].merge(&by_hand);

                    prop_assert_eq!(&via_scribe, &by_hand);
                    prop_assert_eq!(composers[composer].state(), &manual[composer]);
                }
                Op::Gossip { from, to } => {
                    let scribe_delta = composers[from].owed_to(composers[to].state().context());
                    let _ = composers[to].absorb(u32::try_from(from).unwrap(), &scribe_delta);
                    let hand_delta = manual[from].delta_for(manual[to].context());
                    manual[to] = manual[to].merge(&hand_delta);

                    prop_assert_eq!(&scribe_delta, &hand_delta);
                    prop_assert_eq!(composers[to].state(), &manual[to]);
                }
            }
        }
    }
}