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

extern crate alloc;

use alloc::collections::BTreeSet;

use super::super::{Record, Seq, arb_ops, run};
use crate::metis::Dot;
use proptest::prelude::*;

/// Every reachable dot of a rhapsody: the naive walk UP each locus's anchor chain
/// to the origin, the independent oracle for `is_reachable`.
fn reachable_oracle(seq: &Seq, record: &Record) -> BTreeSet<Dot> {
    let mut reachable = BTreeSet::new();
    for &dot in record.woven.keys() {
        if seq.store().locus(dot).is_none() {
            continue;
        }
        // Walk up the anchor chain; reachable iff it terminates at the origin
        // through loci this replica holds.
        let mut cursor = dot;
        let mut seen = BTreeSet::new();
        let reaches = loop {
            let Some(locus) = seq.store().locus(cursor) else {
                break false;
            };
            // An anchor is a raw coordinate: one naming the non-dot zero
            // names no locus, so the chain stops there exactly as a
            // missing locus does (ruling R-91).
            match locus.anchor.dot().map(Dot::try_from) {
                None => break true,
                Some(Err(_)) => break false,
                Some(Ok(anchor)) => {
                    if !seen.insert(cursor) {
                        break false;
                    }
                    cursor = anchor;
                }
            }
        };
        if reaches {
            let _ = reachable.insert(dot);
        }
    }
    reachable
}

proptest! {
    /// C7: `is_reachable` agrees with the naive anchor-chain-to-origin oracle on
    /// every woven dot, at every replica, whether or not the dot is visible (a
    /// placed tombstone is reachable; a dangling child is not).
    #[test]
    fn prop_is_reachable_agrees_with_the_walk_oracle(ops in arb_ops()) {
        let (live, record) = run(&ops);
        for seq in &live {
            let oracle = reachable_oracle(seq, &record);
            for &dot in record.woven.keys() {
                let held = seq.store().locus(dot).is_some();
                let got = seq.store().is_reachable(dot);
                prop_assert_eq!(got, held && oracle.contains(&dot));
            }
        }
    }
}