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
use VersionVector;
/// A [`VersionVector`] witnessed gap-free: a genuine cut, by construction.
///
/// # The trap this type kills
///
/// A [`Stability`](crate::metis::Stability) report is a cut claim: "I hold
/// everything below these counts." A meet of cuts is a cut. A meet that
/// includes an upper bound running past holes over-claims stability, in the
/// unrecoverable direction. Reclamation below an over-claimed watermark
/// destroys the last fillable copy of a hole.
///
/// The honest cut and the over-claiming bound are the same type, a bare
/// [`VersionVector`], indistinguishable at every boundary and unverifiable
/// by the tracker. [`DotSet::floor`](crate::metis::DotSet::floor) made an
/// honest cut *constructible*; `Cut` closes the loop by making it the only
/// thing constructible. The upper-bound-over-holes is not a `Cut` because no
/// path makes one from it.
///
/// # Construction, not assertion
///
/// PRD 0012 rejected a marker newtype, on the grounds that an assertion is
/// not a construction and merely moves the trap to its constructor. So the
/// constructor set here is closed over honest sources
/// ([`bottom`](Self::bottom), [`floor_of`](Self::floor_of),
/// [`delivered_by`](Self::delivered_by), [`common_of`](Self::common_of))
/// plus the closures [`meet`](Self::meet), [`merge`](Self::merge), and
/// [`restrict`](Self::restrict) over cuts already witnessed. No entry takes
/// an unwitnessed vector's word: a decoded vector is a claim and stays one,
/// entering through [`Stability::report`](crate::metis::Stability::report)
/// rather than as a forged `Cut`. The type does not pretend to verify what
/// the tracker cannot.
///
/// The absent doors are pinned by `compile_fail`:
///
/// ```compile_fail
/// use minerva::metis::{Cut, VersionVector};
/// let v = VersionVector::new();
/// // The field is private forever: wrapping an arbitrary vector is exactly
/// // the over-claim `Cut` exists to refuse.
/// let forged = Cut(v);
/// ```
///
/// ```compile_fail
/// use minerva::metis::{Cut, VersionVector};
/// let v = VersionVector::new();
/// // No `From<VersionVector>` (nor `new(vector)`): an assertion door would
/// // be the rejected newtype.
/// let forged = Cut::from(v);
/// ```
///
/// ```compile_fail
/// use minerva::metis::Cut;
/// // No `Default`: a defaulted cut would be a vector-free construction
/// // path. The empty cut is spelled `Cut::bottom()`.
/// let forged = Cut::default();
/// ```
///
/// ```compile_fail
/// use minerva::metis::{Cut, VersionVector};
/// let cut = Cut::bottom();
/// // No `Deref<Target = VersionVector>`: deref would expose every vector
/// // method through the witness. The borrow is the explicit `as_vector`.
/// fn takes_vector(_: &VersionVector) {}
/// takes_vector(&cut);
/// ```
///
/// `serde` is not a dependency, so its absence cannot be pinned by doctest;
/// the attest suite's negative-trait test holds that ban.
///
/// # The closures are theorems
///
/// Pointwise minimum, pointwise maximum, and whole-fiber restriction of
/// gap-free prefixes are gap-free prefixes. Each returns a witness because
/// the closure is a theorem about the vector lattice rather than a re-claim,
/// and each is pinned by property test.
///
/// # The one-way surrender
///
/// [`as_vector`](Self::as_vector) borrows,
/// [`into_vector`](Self::into_vector) surrenders, and surrender is one-way
/// because no vector-taking constructor exists. That is the adoption bridge:
/// `tracker.report(peer, cut.as_vector())` needs no signature change,
/// because the honest report was always a `&VersionVector`. `Cut` changes
/// who may make one, not the report's shape.
///
/// # The honest limitation
///
/// A `Cut` is evidence about the moment of construction. Its sources are
/// monotone, so it never becomes a lie. It can become *stale*, and
/// staleness is the caller's clock. `Cut` makes no freshness claim.
;