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
use crate::metis::{Cut, DotSet};
use super::super::{BOTTOM, DotStore};
use super::Dotted;
impl<S: DotStore> Dotted<S> {
/// The delta this pair owes a peer whose context is `peer_context`: the
/// store fragment the peer has not seen, paired with a context that
/// carries every removal this pair has made. Merging it into the peer
/// converges the peer to exactly what merging this whole pair would
/// (PRD 0015 open question 3, answered S97).
///
/// *Removals ride the context; survivors ride the store.* The context
/// carries every superseded dot whole --- every dot this pair saw and
/// dropped --- never trimmed, plus the coverage of the novel store dots.
/// Trimming removals loses them; carrying shared survivors kills them.
/// Both hazards, and the equivalence law, are
/// `docs/metis-delta-context-law.adoc`.
///
/// The store is [`novel_to`](DotStore::novel_to) the peer's context, so
/// the transfer is support-minimal. A store with a recording plane beside
/// its support --- the sequence store's ordering skeleton --- rides that
/// plane whole per `novel_to`'s selection law, so a caught-up peer's
/// fragment is support-empty rather than bottom.
#[must_use]
pub fn delta_for(&self, peer_context: &DotSet) -> Self {
let store = self.store.novel_to(peer_context);
self.frame_delta(store)
}
/// [`delta_for`](Self::delta_for) under a *recording-possession witness*:
/// the owed delta when the peer states, beside its context, which
/// recording state it holds (its own recording plane as a have-set; the
/// sequence store's [`woven`](crate::metis::Rhapsody::woven) read is the
/// canonical source).
///
/// The context law is [`delta_for`](Self::delta_for)'s verbatim. Only the
/// *store* half changes: selected by
/// [`novel_to_witnessed`](DotStore::novel_to_witnessed), so a store
/// carrying a recording plane withholds exactly what the witness claims
/// instead of shipping the plane whole per probe. Support selection is
/// unchanged, so the equivalence law survives.
///
/// The witness is a claim whose failure directions are both safe:
/// under-claiming over-serves and the grow-only recording union absorbs
/// it, over-claiming starves only the claimant. Hence a bare [`DotSet`]
/// is the right trust grade.
#[must_use]
pub fn delta_for_witnessed(&self, peer_context: &DotSet, peer_recording: &DotSet) -> Self {
let store = self.store.novel_to_witnessed(peer_context, peer_recording);
self.frame_delta(store)
}
/// Frames a selected store fragment as a covered owed delta under the
/// removal discipline both public reads share: removals ride whole,
/// surviving coverage rides the fragment. The held set reads through
/// [`support`](DotStore::support), the maintained have-set form where
/// the store keeps one.
fn frame_delta(&self, store: S) -> Self {
let held = self.store.support();
let mut context = DotSet::new();
for dot in self.context.difference(&held) {
let _ = context.insert(dot);
}
for dot in store.dots() {
let _ = context.insert(dot);
}
Self { store, context }
}
/// The whole-state delta against a peer whose gap-free floor is witnessed by
/// `peer`: this pair's survivors carried under a context *floored* at the
/// cut, so the context frame folds a contiguous prefix into a single floor
/// instead of parking it as a per-dot exception run.
///
/// The whole-state read for anti-entropy when a witnessed peer floor is
/// in hand. Complementary to [`delta_for`](Self::delta_for) rather than
/// an upgrade: that one targets a peer's *exact* context and trims the
/// store; this targets a *floor* and buys the context frame instead.
///
/// The context is seeded at the cut, capped at this pair's own knowledge
/// so it never claims an unseen dot, with every removal riding on top.
/// The store carried is the *whole* survivor store, which is forced
/// rather than wasteful, and the parameter is a [`Cut`] rather than a
/// bare vector because the seed asserts gap-freedom below itself. Both
/// arguments, the removal split at the cut, and the equivalence law are
/// `docs/metis-delta-context-law.adoc`.
#[must_use]
pub fn delta_for_since(&self, peer: &Cut) -> Self {
// The whole survivor store: a floored context covers every survivor at
// or below the cut, and a covered survivor absent from the store would
// read as seen-and-dropped (the mirror hazard), so every survivor rides.
// `novel_to(bottom)` is the store's own canonical rebuild (nothing is
// covered by the empty set), the value-opaque way to carry it whole.
let store = self.store.novel_to(&BOTTOM);
let held = self.store.support();
// Seed the context at the witnessed floor, capped at this pair's own
// knowledge so it never claims a dot this pair has not seen (which it
// could not re-supply, and would thereby fabricate a peer's removal).
// The fold this buys: the contiguous prefix folds into one floor on
// `insert` instead of parking as an exception run, the frame win.
let mut context = peer.to_have_set().intersect(&self.context);
// Every removal rides whole (context dots this pair no longer holds),
// never trimmed; one at or below the cut folds into the seed, one above
// it extends the frame.
for dot in self.context.difference(&held) {
let _ = context.insert(dot);
}
// The surviving coverage rides the store, so a survivor the seed covers
// is matched by a store dot and not superseded out from under the peer.
for dot in store.dots() {
let _ = context.insert(dot);
}
Self { store, context }
}
}