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

use core::cmp::Ordering;

use super::Cut;
use crate::metis::VersionVector;

impl Cut {
    /// The pointwise-minimum cut: the greatest cut below both.
    ///
    /// Closed by *theorem*, not claim: a station's prefix in the meet is the
    /// smaller of two gap-free prefixes, which is itself a gap-free prefix, so
    /// the result is gap-free with no fresh construction. Agrees exactly with
    /// [`VersionVector::meet`] on the witnessed vectors.
    #[must_use]
    pub fn meet(&self, other: &Self) -> Self {
        Self(self.0.meet(&other.0))
    }

    /// The pointwise-maximum cut: the least cut above both.
    ///
    /// Closed by *theorem*, not claim: a station's prefix in the join is the
    /// larger of two gap-free prefixes (and every dot below the larger is below
    /// one side or the other, so no hole is introduced), so the result is
    /// gap-free with no fresh construction. Agrees exactly with
    /// [`VersionVector::merge`] on the witnessed vectors.
    #[must_use]
    pub fn merge(&self, other: &Self) -> Self {
        Self(self.0.merge(&other.0))
    }

    /// The restriction to a sub-roster: the same prefixes on the stations
    /// `roster` names, nothing anywhere else.
    ///
    /// Closed by *theorem*, not claim: restriction selects whole per-station
    /// fibers and never looks inside one, so each kept prefix stays exactly the
    /// gap-free prefix it was and the dropped stations introduce no hole. Agrees
    /// exactly with [`VersionVector::restrict`] on the witnessed vector.
    #[must_use]
    pub fn restrict(&self, roster: impl IntoIterator<Item = u32>) -> Self {
        Self(self.0.restrict(roster))
    }

    /// The *owed vector* against another cut: the co-Heyting residual
    /// [`VersionVector::difference`], "the least gossip that raises `other` to
    /// cover `self`."
    ///
    /// # Why this returns a `VersionVector` and not a `Cut`
    ///
    /// The residual is exact here for the same reason
    /// [`VersionVector::difference`] is exact on cuts. PRD 0014's Galois
    /// connection pins the answer: `a.difference(&b) <= x` iff `a <=
    /// b.merge(&x)`. Both operands are genuine cuts, which makes the *owed
    /// events* the contiguous per-station spans `(other, self]` (the adjoint
    /// ledger's residual section). But exactness is not gap-freedom, and the
    /// residual is deliberately not typed `Cut`, because it is not a cut in
    /// general.
    ///
    /// A `Cut` witnesses a *down-set*: "I hold everything below these counts,
    /// from the origin up." The residual is the opposite shape. Where `self`
    /// leads, [`VersionVector::difference`] carries `self`'s own count (the
    /// *claim* `other` must be raised to), so the vector's coordinate is the
    /// *top* of the owed span, not a prefix length. The owed dots are
    /// `(other.get(s), self.get(s)]`, which start above `other`'s floor, not at
    /// the origin: embedding that coordinate as a cut would assert every dot
    /// below it is owed, over-claiming exactly the run `other` already holds.
    /// The residual is a per-station claim (one counter, "raise to here"), not a
    /// witnessed prefix, so it stays a bare vector and the caller reads the
    /// genuine owed *dots* through
    /// [`DotSet::difference`](crate::metis::DotSet::difference) on the two
    /// have-set embeddings, which enumerates exactly that span.
    ///
    /// Correctness beats symmetry: the closures ([`meet`](Self::meet),
    /// [`merge`](Self::merge), [`restrict`](Self::restrict)) return `Cut` because
    /// their outputs *are* cuts by theorem; the residual's output is not, so it
    /// surrenders the witness the way [`into_vector`](Self::into_vector) does.
    #[must_use]
    pub fn difference(&self, other: &Self) -> VersionVector {
        self.0.difference(&other.0)
    }
}

/// Pointwise causal order, delegating to [`VersionVector`]'s partial order: a
/// `Cut` precedes another exactly when its witnessed vector does.
///
/// The order is *preserved by every closure*. [`meet`](Cut::meet) lands at or
/// below both operands, [`merge`](Cut::merge) at or above both, and
/// [`restrict`](Cut::restrict) preserves `<=` (PRD 0013's base-change law), so
/// the lattice the cuts live in is the vector lattice read through the witness,
/// with no fresh order to reason about. Partial, not total: two cuts can be
/// concurrent (each leads the other on some station), exactly as their vectors
/// are, which is why this is `PartialOrd` and not `Ord`.
impl PartialOrd for Cut {
    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
        self.0.partial_cmp(&other.0)
    }
}