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

extern crate alloc;

use crate::metis::{Cut, Dot, DotSet};
use alloc::vec::Vec;
use proptest::prelude::*;

mod lattice;
mod sources;
mod views;

fn arb_dots() -> impl Strategy<Value = Vec<(u32, u64)>> {
    prop::collection::vec((0u32..4, 0u64..12), 0..24)
}

fn arb_subroster() -> impl Strategy<Value = Vec<u32>> {
    prop::collection::vec(0u32..6, 0..6)
}

fn have(dots: &[(u32, u64)]) -> DotSet {
    let mut set = DotSet::new();
    for &pair in dots {
        // A drawn zero counter is no dot and cannot cross into the identity
        // type: the same no-op the door's zero refusal gave (ruling R-91).
        if let Ok(dot) = Dot::try_from(pair) {
            let _ = set.insert(dot);
        }
    }
    set
}

fn arb_cut() -> impl Strategy<Value = Cut> {
    arb_dots().prop_map(|dots| Cut::floor_of(&have(&dots)))
}

fn is_genuine_cut(cut: &Cut) -> bool {
    let vector = cut.as_vector();
    DotSet::from_cut(vector).floor() == *vector
}