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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
extern crate alloc;
use alloc::collections::BTreeMap;
use alloc::vec::Vec;
use crate::metis::Retired;
use super::Rhapsody;
use super::maintenance::placed_anchor;
use super::placement::Dot;
impl Rhapsody {
/// Excises order tombstones: every dot that is (a) invisible here, (b)
/// named by `retired`, and (c) sterile, meaning no locus in the skeleton
/// anchors to it. `retired` is the [`Retired`] witness: removed and
/// applied at EVERY replica that will ever write again. The excision
/// applies transitively: a dead unbranched chain is excised tip-first,
/// until a survivor, a non-retired dot, or an anchored dot stops it.
/// Returns how many loci were excised.
///
/// # Why the claim is typed
///
/// An over-claim --- naming a dot some replica still shows or will still
/// anchor to --- strands that replica's future locus as a dangling anchor
/// at every condensed replica, invisible in [`order()`](Self::order).
/// Stranded text, the unrecoverable direction. Under-claiming merely
/// retains skeleton.
///
/// Removal deltas mint no dot, so "everyone has applied this deletion" is
/// *not* derivable from the crate's mint-based stability watermark. It is
/// application evidence only a deployment can gather --- an ack round, an
/// app-level epoch, a quorum sweep --- so minerva supplies the mechanism
/// and the caller supplies the claim, through a
/// [`Retirement`](crate::metis::Retirement) meet or the audited
/// [`Retired::trust`](crate::metis::Retired::trust) escape. A bare
/// [`DotSet`](crate::metis::DotSet) cannot reach this path: the witness
/// is precisely the difference between "removed locally" and "removed and
/// applied everywhere".
///
/// *That evidence alone is not sufficient*, and the missing half is a
/// write discipline. [`weave`](Self::weave) accepts dangling anchors, so
/// a replica that has acknowledged removing `d` may still anchor a future
/// element to it, and that element is unreachable in
/// [`order()`](Self::order) at every replica that condensed `d`. Excision
/// is permanently safe only when writers choose anchors among *visible*
/// elements and no write is concurrent with the retirement knowledge.
///
/// A visible dot is never excised even when `retired` names it. Visible
/// here contradicts removed-everywhere, so the claim is wrong for that dot
/// and the mechanism declines it silently. Visibility and the pair
/// contexts are untouched; this trims the skeleton coordinate only.
///
/// # Hygiene, not protocol
///
/// A merge with an uncondensed peer re-learns excised loci, since the
/// skeleton union is grow-only; the survivor law keeps the dot invisible,
/// and a repeat `condense` with the same claim excises it again.
/// [`order()`](Self::order) is invariant under the whole cycle.
///
/// # Shape and cost
///
/// Sterility is decided without recursion, since skeleton depth is
/// attacker-controllable. One pass builds an `anchored_by` count per dot;
/// a candidate is a dot with count zero that is invisible and retired;
/// and an explicit worklist excises each candidate, decrements its
/// anchor's count, and enqueues that anchor when it falls sterile.
///
/// Each locus is enqueued at most once, so the call is `O(n log n)` for
/// `n` woven elements. Only leaf-first sterile excision: collapsing a
/// chain of still-anchored tombstones into one gap locus is a further
/// compaction this does not attempt.
#[must_use]
pub fn condense(&mut self, retired: &Retired) -> usize {
// The witness unwraps to the claimed have-set only inside the
// mechanism; a caller cannot reach this bare set.
let retired = retired.dots();
// One pass: how many skeleton loci name each dot as their anchor.
// A dot absent from this map has count zero (sterile: nothing anchors
// to it). The origin (`None`) is never a dot, so it never keys here.
let mut anchored_by: BTreeMap<Dot, usize> = BTreeMap::new();
for (_, locus) in self.skeleton.iter() {
// Sterility is side-agnostic: a dot is fertile if ANY locus (Before
// or After) anchors to it, so count by the anchoring dot (S127).
// A non-dot anchor coordinate names no woven element, so it can
// key no candidate and its tally would never be read: the funnel
// drops it here rather than carrying a dead row (ruling R-91).
if let Some(anchor) = locus.anchor.dot().and_then(|raw| Dot::try_from(raw).ok()) {
*anchored_by.entry(anchor).or_insert(0) += 1;
}
}
// A dot qualifies for excision when it is invisible here (the visible
// guard: visible contradicts removed-everywhere, decline it), named by
// the caller's claim, and sterile (count zero: no live child locus).
let qualifies = |dot: Dot, anchored_by: &BTreeMap<Dot, usize>| -> bool {
!self.visible.contains(dot)
&& retired.contains(dot)
&& anchored_by.get(&dot).copied().unwrap_or(0) == 0
};
// Seed the worklist with every currently sterile qualifier.
let mut worklist: Vec<Dot> = self
.skeleton
.iter()
.map(|(dot, _)| dot)
.filter(|&dot| qualifies(dot, &anchored_by))
.collect();
let mut excised = 0usize;
while let Some(dot) = worklist.pop() {
// Re-check under the current counts: a dot enqueued earlier may
// have been an anchor whose child was excised meanwhile, but the
// seed already required count zero, and counts only fall, so this
// stays true; the guard is belt for the transitive enqueue below.
let Some(locus) = self.skeleton.remove(dot) else {
continue;
};
excised += 1;
// Maintain the child plane: this excised dot leaves its anchor's
// sibling bucket (S116, C8 invalidation hook for condense; since
// arc 11 phase four the removal runs after the plane entry left,
// because an implicit chain child's bucket IS its plane entry).
// An excised dot is sterile, so it keys no bucket of its own to
// drop. NOTE (S115 merge): if condense's signature changes to
// take a witness type in place of `&DotSet`, this
// index-maintenance block is unaffected; keep it beside the
// `skeleton.remove` above.
let tail_change = self.children.remove(&self.skeleton, locus.anchor, dot);
// Maintain the placement set (S183): the excised dot leaves it if
// it was dangling. Sterility means nothing anchors to the excised
// dot, so no OTHER dot's placement can change here; a locus that
// arrives anchored to it later parks as dangling on arrival,
// exactly the stranded-anchor hazard the over-claim prose above
// records.
let _ = self.unplaced.remove(&dot);
// Maintain the recording have-set: the excised locus is no longer
// held, so the witness must stop claiming it (a condensed replica
// that kept claiming would starve itself of the re-learn a merge
// with an uncondensed peer provides).
let _ = self.woven.remove(dot);
// Maintain the order thread (S200): the excised slot leaves the
// positional view (an unplaced excision holds no slot and the
// removal refuses untouched; visibility aggregates cannot move,
// since only an invisible dot qualifies for excision).
let held_slot = self.thread.remove_slot(dot);
// A sterile placed dot is a leaf in both dynamic endpoint
// forests. If it was its parent's last child on this side,
// replace that one edge before retiring its node.
if held_slot && let super::children::TailChange::Replaced(child) = tail_change {
let linked = match locus.anchor {
super::Anchor::Origin => true,
super::Anchor::Before(parent) => self
.thread
.replace_region_start(placed_anchor(parent), child),
super::Anchor::After(parent) => {
self.thread.replace_region_end(placed_anchor(parent), child)
}
};
debug_assert!(linked, "a placed parent has a region node");
}
if held_slot {
let removed = self.thread.remove_region_dot(dot);
debug_assert!(removed, "every placed slot has a region node");
}
// Excising this locus drops its edge to its anchor dot: decrement,
// and if the anchor just fell sterile and qualifies, enqueue it
// (tip-first up the dead unbranched chain). Each locus is removed
// at most once, so it enters the worklist at most once. Side-agnostic:
// the edge is to the anchoring dot, whichever side the locus hung on.
if let Some(anchor) = locus.anchor.dot().and_then(|raw| Dot::try_from(raw).ok()) {
if let Some(count) = anchored_by.get_mut(&anchor) {
*count = count.saturating_sub(1);
}
if qualifies(anchor, &anchored_by) {
worklist.push(anchor);
}
}
}
excised
}
}