minerva 0.2.0

Causal ordering for distributed systems
//! The kind-read laws: `kinds_present` against an independent reference
//! recomputation, and the `sole` coincidences (none, one, plurality).

extern crate alloc;

use alloc::vec::Vec;

use proptest::prelude::*;

use crate::metis::{DotStore, Kind, NodeContent};

use super::super::TestNode;
use super::{arb_ops, run, settle};

/// The reference evidence read, re-derived from the raw component accessors
/// so a drift in `kinds_present` cannot hide behind its own definition: tag
/// claims, plus each shape with surviving support, in the fixed kind order.
fn reference_kinds(node: &TestNode) -> Vec<Kind> {
    let mut kinds: Vec<Kind> = node.tag().values().copied().collect();
    if node.register().values().next().is_some() {
        kinds.push(Kind::Register);
    }
    if node
        .children()
        .iter()
        .any(|(_, child)| DotStore::dots(child).next().is_some())
    {
        kinds.push(Kind::Map);
    }
    if node.sequence().visible_len() > 0 {
        kinds.push(Kind::Sequence);
    }
    kinds.sort_unstable();
    kinds.dedup();
    kinds
}

proptest! {
    /// `kinds_present` is exactly the reference evidence, and `sole` is its
    /// case split: `Ok(None)` on no evidence, the matching component on a
    /// singleton, the full witness on a plurality. Checked at every block of
    /// every replica a generated tape can reach.
    #[test]
    fn prop_kind_reads_match_the_reference(ops in arb_ops()) {
        let mut fleet = run(&ops);
        settle(&mut fleet);
        for author in &fleet {
            for (_, block) in author.state().store().children() {
                let kinds = block.kinds_present();
                prop_assert_eq!(kinds.iter().collect::<Vec<_>>(), reference_kinds(block));
                match block.sole() {
                    Ok(None) => prop_assert!(kinds.is_empty()),
                    Ok(Some(NodeContent::Register(_))) => {
                        prop_assert_eq!(kinds.sole(), Some(Kind::Register));
                    }
                    Ok(Some(NodeContent::Map(_))) => {
                        prop_assert_eq!(kinds.sole(), Some(Kind::Map));
                    }
                    Ok(Some(NodeContent::Sequence(_))) => {
                        prop_assert_eq!(kinds.sole(), Some(Kind::Sequence));
                    }
                    Err(plurality) => {
                        prop_assert!(kinds.len() >= 2);
                        prop_assert_eq!(plurality.kinds, kinds);
                    }
                }
            }
        }
    }
}