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

use crate::metis::DotSet;

/// Evidence that a set of removed dots has been applied at *every* roster
/// member.
///
/// The one claim [`Rhapsody::condense`](crate::metis::Rhapsody::condense) and
/// [`Composer::condense`](crate::metis::Composer::condense) accept. The inner
/// [`DotSet`] is private, so the only ways to build a `Retired` are
/// [`Retirement::retired`](crate::metis::Retirement::retired) (the honest meet
/// across a fixed roster) and the audited [`trust`](Self::trust) escape. A bare
/// `DotSet` no longer condenses: the type is the difference between "dots I have
/// removed locally" and "dots removed and applied everywhere", and only the
/// latter is safe to excise.
///
/// A bare have-set cannot reach
/// [`Rhapsody::condense`](crate::metis::Rhapsody::condense); the over-claim
/// that stranded a laggard's anchor is now unconstructible:
///
/// ```compile_fail
/// use minerva::metis::{Dot, DotSet, Rhapsody};
/// let mut rhapsody = Rhapsody::new();
/// let mut claim = DotSet::new();
/// claim.insert(Dot::from_parts(1, 1).unwrap());
/// // The claim is a bare DotSet, not a witnessed Retired: this does not compile.
/// let _ = rhapsody.condense(&claim);
/// ```
///
/// The honest path takes a witness built by
/// [`Retirement`](crate::metis::Retirement) (or, with the burden documented,
/// [`trust`](Self::trust)):
///
/// ```
/// use minerva::metis::{Dot, DotSet, Retirement, Rhapsody};
/// let mut retirement = Retirement::new([1u32]);
/// let mut applied = DotSet::new();
/// applied.insert(Dot::from_parts(1, 1).unwrap());
/// retirement.acknowledge(1, &applied).unwrap();
/// let mut rhapsody = Rhapsody::new();
/// let _excised = rhapsody.condense(&retirement.retired());
/// ```
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Retired(DotSet);

impl Retired {
    /// Builds the witness from the retirement tracker's roster meet.
    pub(super) const fn from_meet(dots: DotSet) -> Self {
        Self(dots)
    }

    /// Borrows the claimed dots, for the mechanism that consumes the claim.
    pub(crate) const fn dots(&self) -> &DotSet {
        &self.0
    }

    /// The audited escape: asserts, on the caller's word, that every dot in
    /// `claim` has been removed and applied at every replica that will ever
    /// write again.
    ///
    /// The removal-side counterpart of
    /// [`Scoped::forget`](crate::metis::Scoped::forget) and
    /// [`Cut::into_vector`](crate::metis::Cut::into_vector): the name is the
    /// warning. [`Retirement`](crate::metis::Retirement) gathers this claim
    /// honestly from per-member acknowledgements; `trust` bypasses the tracker
    /// for a caller who has gathered application evidence some other way. The
    /// studio's `honest_retirement` global-oracle scan (readable only because
    /// the simulation holds the global state) is the documented example: it
    /// reads every replica, keeps the dots invisible at all of them, and wraps
    /// the result here, standing in for the deployment's ack round or quorum
    /// sweep.
    ///
    /// The burden is total and unrecoverable: an over-claim (naming a dot a
    /// laggard still shows or will still anchor to) strands that laggard's
    /// future thread as a dangling anchor at every condensed replica, invisible
    /// in [`order()`](crate::metis::Rhapsody::order). Prefer
    /// [`Retirement`](crate::metis::Retirement) where the roster is known; reach
    /// for `trust` only when the evidence lives outside this type.
    #[must_use]
    pub const fn trust(claim: DotSet) -> Self {
        Self(claim)
    }
}