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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

use core::cmp::Ordering;

use super::Gate;

/// The endpoint at which an observable [`Gate`] law failed.
///
/// `#[non_exhaustive]` so a future law's endpoint is additive.
#[non_exhaustive]
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub enum GateLawPoint {
    /// The lower progress supplied to [`check_gate_laws`].
    Lower,
    /// The upper progress supplied to [`check_gate_laws`].
    Upper,
}

/// A malformed case or observable [`Gate`] law violation.
///
/// `#[non_exhaustive]` so a future law's violation is additive.
#[non_exhaustive]
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, thiserror::Error)]
pub enum GateLawCheckError {
    /// The supplied progress pair descends instead of rising.
    #[error("lower progress is greater than upper progress")]
    ProgressDescends,
    /// The supplied progress states are incomparable.
    #[error("lower and upper progress are incomparable")]
    ProgressIncomparable,
    /// [`Gate::advance`] did not preserve the information order.
    #[error("advance did not monotonically increase {at:?} progress")]
    AdvanceNotMonotone {
        /// The progress endpoint whose advance failed.
        at: GateLawPoint,
    },
    /// [`Gate::deliverable`] and [`Gate::stale`] both held.
    #[error("deliverable and stale overlap at {at:?} progress")]
    DeliverableAndStale {
        /// The progress endpoint where the regions overlapped.
        at: GateLawPoint,
    },
    /// A stale event became non-stale as progress rose.
    #[error("stale is not terminal across the progress pair")]
    StaleNotTerminal,
    /// A stable event returned to the waiting region as progress rose.
    #[error("deliverable or stale is not upward closed across the progress pair")]
    StableNotUpwardClosed,
}

/// Checks one caller-generated case against the observable [`Gate`] laws.
///
/// `lower` and `upper` must be comparable progress states in ascending
/// information order. The check rejects malformed pairs, verifies that
/// [`Gate::advance`] rises from each endpoint, and checks terminal stale,
/// disjoint stable regions, and stable up-closure for `sender` and `dep`.
/// Callers retain control of case generation and can use this function from
/// any property-testing framework.
///
/// This function cannot establish that `advance` is called only for events the
/// gate admitted. That dynamic obligation requires a proof at the delivery
/// machine or combinator boundary.
///
/// # Errors
///
/// Returns [`GateLawCheckError`] when the progress pair is malformed or an
/// observable law does not hold for this case.
pub fn check_gate_laws<G: Gate>(
    lower: &G::Progress,
    upper: &G::Progress,
    sender: u32,
    dep: &G::Dep,
) -> Result<(), GateLawCheckError>
where
    G::Progress: Clone + PartialOrd,
{
    match lower.partial_cmp(upper) {
        Some(Ordering::Less | Ordering::Equal) => {}
        Some(Ordering::Greater) => return Err(GateLawCheckError::ProgressDescends),
        None => return Err(GateLawCheckError::ProgressIncomparable),
    }

    let mut advanced_lower = lower.clone();
    G::advance(&mut advanced_lower, sender, dep);
    if !matches!(
        lower.partial_cmp(&advanced_lower),
        Some(Ordering::Less | Ordering::Equal)
    ) {
        return Err(GateLawCheckError::AdvanceNotMonotone {
            at: GateLawPoint::Lower,
        });
    }

    let mut advanced_upper = upper.clone();
    G::advance(&mut advanced_upper, sender, dep);
    if !matches!(
        upper.partial_cmp(&advanced_upper),
        Some(Ordering::Less | Ordering::Equal)
    ) {
        return Err(GateLawCheckError::AdvanceNotMonotone {
            at: GateLawPoint::Upper,
        });
    }

    let lower_deliverable = G::deliverable(lower, sender, dep);
    let lower_stale = G::stale(lower, sender, dep);
    let upper_deliverable = G::deliverable(upper, sender, dep);
    let upper_stale = G::stale(upper, sender, dep);

    if lower_deliverable && lower_stale {
        return Err(GateLawCheckError::DeliverableAndStale {
            at: GateLawPoint::Lower,
        });
    }
    if upper_deliverable && upper_stale {
        return Err(GateLawCheckError::DeliverableAndStale {
            at: GateLawPoint::Upper,
        });
    }
    if lower_stale && !upper_stale {
        return Err(GateLawCheckError::StaleNotTerminal);
    }
    if (lower_deliverable || lower_stale) && !(upper_deliverable || upper_stale) {
        return Err(GateLawCheckError::StableNotUpwardClosed);
    }

    Ok(())
}