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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
use core::cmp::Ordering;
use super::VersionVector;
impl VersionVector {
/// Returns the least upper bound of `self` and `other`: the pointwise maximum
/// over every station either has observed.
///
/// The lattice join. It is commutative, associative, and idempotent, and it
/// models a node learning everything both vectors knew.
#[must_use]
pub fn merge(&self, other: &Self) -> Self {
let mut counters = self.counters.clone();
for (&station, &count) in &other.counters {
// other is canonical (count > 0), so no branch inserts a zero.
let _ = counters
.entry(station)
.and_modify(|c| *c = (*c).max(count))
.or_insert(count);
}
Self { counters }
}
/// Returns the greatest lower bound of `self` and `other`: the pointwise
/// minimum, keeping only the stations both have observed.
///
/// The lattice meet, the order dual of [`merge`](Self::merge); together they
/// make the vector order a distributive lattice (pointwise `min` / `max` over
/// counts), exercised by the absorption and distributivity properties. Where
/// `merge` models a node learning everything both vectors knew, `meet` models
/// what two vectors *agree* on: the greatest knowledge neither disputes.
/// Commutative, associative, idempotent.
///
/// Its distinguished use is the *stability watermark* `min_n D_n` over
/// every node's delivered cut ([`Stability`](crate::metis::Stability), PRD
/// 0011). An event at or below the meet of all delivered vectors is
/// delivered everywhere, so it is safe to forget. That watermark is a meet
/// over a *declared* family. The binary operation here is total and
/// neutral. The tracker exists to hold the family honest: a meet over
/// "peers heard from so far" over-approximates stability, which is the
/// unsafe direction.
///
/// Canonical form is preserved for free: a station absent from either side has
/// pointwise minimum `0` (`min(x, 0) == 0`), so it stays absent.
#[must_use]
pub fn meet(&self, other: &Self) -> Self {
let counters = self
.counters
.iter()
.filter_map(|(&station, &count)| {
let both = count.min(other.get(station));
(both > 0).then_some((station, both))
})
.collect();
Self { counters }
}
/// Returns the *owed set*: the least vector whose [`merge`](Self::merge)
/// into `other` covers `self`. The co-Heyting residual of the vector
/// lattice, "the least gossip that makes you cover me."
///
/// The *difference read* (PRD 0014), the anti-entropy question between the
/// two folds: [`merge`](Self::merge) answers "what do we jointly know" and
/// [`meet`](Self::meet) "what do we agree on"; `difference` answers "what
/// do I owe you." Its universal property specifies it: the Galois
/// connection `a.difference(&b) <= x` iff `a <= b.merge(&x)`. That
/// connection fixed its laws before the method existed. It is the adjoint
/// ledger's residual section, and this method's property suite converts it
/// from *predicted* to *tested*. Three laws follow:
///
/// * bottom exactly when the debt is clear: `a.difference(&b)` is empty
/// iff `a <= b`;
/// * repaying the debt reaches exactly the join, no more:
/// `b.merge(&a.difference(&b)) == a.merge(&b)`;
/// * owed against two creditors folds their knowledge:
/// `a.difference(&b).difference(&c) == a.difference(&b.merge(&c))`.
///
/// # The residual carries claims, never subtracted counters
///
/// Where `self` leads, the result carries `self`'s own count (the claim
/// `other` must be raised to), not the numeric difference. A subtracted
/// counter type-checks and is wrong: it is not a vector coordinate, and
/// merging it repays the wrong debt (the ledger's shape warning; pinned by
/// example test). The owed *events* are the per-station spans
/// `(other.get(s), self.get(s)]`, whose sizes are the subtractions;
/// [`DotSet::difference`](crate::metis::DotSet::difference) enumerates
/// exactly those dots when both sides are genuine cuts.
///
/// Total, and canonical for free: an entry appears only where `self`
/// strictly leads, so the support stays inside `self`'s and no zero is
/// stored. Commutes exactly with [`restrict`](Self::restrict), being
/// computed per station from that station's coordinates alone (the PRD
/// 0013 R2 base-change law, property-tested). Like every read here it
/// computes over *claims*: whether `other` was an honest cut or a
/// liveness high-water is the caller's standing vector-meaning hazard,
/// unchanged.
#[must_use]
pub fn difference(&self, other: &Self) -> Self {
let counters = self
.counters
.iter()
.filter_map(|(&station, &count)| {
(count > other.get(station)).then_some((station, count))
})
.collect();
Self { counters }
}
/// Returns `true` if `self` strictly causally precedes `other`: every station
/// is `<=` and at least one is strictly `<`.
#[must_use]
pub fn happens_before(&self, other: &Self) -> bool {
self.partial_cmp(other) == Some(Ordering::Less)
}
/// Returns `true` if the two vectors are concurrent: neither causally precedes
/// the other. Equivalent to `self.partial_cmp(other).is_none()`.
#[must_use]
pub fn concurrent(&self, other: &Self) -> bool {
self.partial_cmp(other).is_none()
}
}
/// The causal relation, decided pointwise over the union of stations:
/// `Less`/`Greater` for a strict happens-before, `Equal` for identical vectors,
/// and `None` for concurrent (each leads the other somewhere).
impl PartialOrd for VersionVector {
fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
let mut self_leads = false;
let mut other_leads = false;
for (&station, &here) in &self.counters {
match here.cmp(&other.get(station)) {
Ordering::Greater => self_leads = true,
Ordering::Less => other_leads = true,
Ordering::Equal => {}
}
}
// A station present in `other` but not `self` reads as `0` here against a
// positive count there (both maps are canonical), so `other` leads.
if other
.counters
.keys()
.any(|station| !self.counters.contains_key(station))
{
other_leads = true;
}
match (self_leads, other_leads) {
(false, false) => Some(Ordering::Equal),
(true, false) => Some(Ordering::Greater),
(false, true) => Some(Ordering::Less),
(true, true) => None,
}
}
}