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

//! The in-tree payload store conforms to the open axis, with values checked.
//!
//! `DotFun<V>` is the production-grade generalization of the test-only
//! `Inscribed` store (`src/metis/tests/causal_store/foreign/`): the same
//! multi-value register shape, now shipped. These properties re-drive the
//! trait laws against it with content genuinely exercised.

extern crate alloc;

use alloc::string::String;
use alloc::vec::Vec;

use super::super::support::dot;
use crate::metis::{DotFun, DotSet, DotStore};
use proptest::prelude::*;

mod accessors;
mod merge;
mod reads;

/// A covered pair carrying the [`crate::metis::Dotted`] precondition.
#[derive(Clone, Debug)]
struct Covered {
    store: DotFun<String>,
    context: DotSet,
}

impl Covered {
    fn new(store: DotFun<String>, context: DotSet) -> Self {
        let covered = Self { store, context };
        for held in covered.store.dots() {
            let (station, counter) = (held.station(), held.counter());
            assert!(
                covered.context.contains(held),
                "DotFun property fixture is uncovered at ({station}, {counter})"
            );
        }
        covered
    }

    fn store(&self) -> &DotFun<String> {
        &self.store
    }

    fn context(&self) -> &DotSet {
        &self.context
    }
}

/// A seed for one covered pair: seen dots plus whether each dot survives.
type Seed = Vec<((u32, u64), bool)>;

fn arb_seed() -> impl Strategy<Value = Seed> {
    prop::collection::vec(((0u32..3, 1u64..8), prop::bool::ANY), 0..12)
}

/// A deterministic value for a dot, so equal dots imply equal strings.
fn value_for(station: u32, counter: u64) -> String {
    alloc::format!("v{station}-{counter}")
}

/// Builds a covered `DotFun<String>` pair from a seed.
fn covered(seed: &Seed) -> Covered {
    let mut context = DotSet::new();
    let mut store = DotFun::new();
    for &((station, counter), keep) in seed {
        let _ = context.insert(dot(station, counter));
        if keep {
            let _ = store.insert(dot(station, counter), value_for(station, counter));
        }
    }
    Covered::new(store, context)
}