= Module: metis::rhapsody
:toc: macro
:toclevels: 2
Design notes for the `metis::rhapsody` submodule, co-located with its source files. This
is the implementer's view of the *sequence store*: the two coordinates it carries, the
reads that recover a document order from them, and the invariants a change must not
break. Path refs in this note are relative to this directory (`src/metis/rhapsody/`):
`mod.rs` owns the carried value, construction, and direct reads; `maintenance.rs`
owns weaving and general derived-coordinate placement maintenance; `reparent.rs`
owns movement re-parenting and its typed transition; `identity/mod.rs` the interned
identity plane (the skeleton's carrier, S194; run-coalesced since S199, arc 11 phase
two), `thread/mod.rs` the order-thread facade, `thread/arena.rs` its fragment arena
(the positional plane, S200, arc 11 phase three), `thread/arena/mutate.rs` its
point and run mutation (S261), `thread/arena/reads.rs` its positional reads
(S260), `thread/region.rs` its
run-coalesced endpoint coordinate (S255/S256), and `thread/arena/splice.rs` the
fragment-grade range carrier (S259),
`placement.rs` the public
placement algebra, `traversal.rs` the order reads, `extent.rs` the span-boundary
vocabulary and projection (`Verge` / `Extent` / `extent`, PRD 0021, S195),
`possession/mod.rs` the paged occupancy plane (the visible plane's possession-diff
shell, S205),
`recension/mod.rs` the movement replay read (`Recension` / `recension`, PRD 0022,
S196), `recension/collation.rs` its maintained possession-diff and suffix-replay
implementation (S254), `recension/batch.rs` its borrow-scoped forward movement-write capability
and `recension/batch/tests.rs` that capability's phase suite (S253),
`recension/cycle.rs` its shared exact-or-bounded cycle verdict core (S252),
and `recension/profile.rs` its feature-gated timing schema (S251),
`condense.rs` the typed excision,
`store.rs` the `DotStore` instance, and `wire/` the codecs (the canonical v2 frame,
plus `wire/snapshot/` since S197, the run-compressed sibling of PRD 0023).
The Rhapsody is the first sequence-shaped instance of the open `DotStore` axis
(xref:../mod.adoc[the parent `metis` note], the causal store section). Product-level
intent lives in xref:../../../docs/prd/0017-metis-rhapsody-sequence-store.adoc[PRD 0017];
the kernel it instantiates (the causal pair, the survivor law, dot assignment) is
xref:../../../docs/prd/0015-metis-causal-store-algebra.adoc[PRD 0015]; the *visible*
coordinate is the have-set of
xref:../../../docs/prd/0012-metis-dot-set-exact-have-set.adoc[PRD 0012] /
xref:../../../docs/prd/0016-metis-have-set-wire-frame.adoc[PRD 0016]. The anchoring
rule the visual reads implement (the "catX" surprise diagnosed as a rank fact, not an
anchor bug; the S127 sided anchor that closes the backward-run interleaving) is analyzed in
xref:../../../docs/metis-rhapsody-anchoring.adoc[the rhapsody-anchoring note]; the sided
anchor slice itself is
xref:../../../docs/prd/0018-metis-rhapsody-sided-anchor.adoc[PRD 0018].
toc::[]
== Responsibility
The kernel supplies identity, causality, and removal; the Rhapsody supplies *order*.
It answers two questions a plain replicated register cannot: in what sequence do the
elements read, and how does that sequence survive concurrent editing and deletion. Two
reasons to change this submodule: a change to how the order is defined (the skeleton,
the `Anchor`, the `Locus`, the sibling rule, the in-order `order` walk), or a change to
how the two coordinates merge, restrict, or serialize.
The submodule is pure `no_std`; every allocating source file imports `alloc` explicitly
(`mod.rs:3`, `maintenance.rs:3`, `reparent.rs:3`, `identity/mod.rs:74`,
`thread/arena.rs:55`, `thread/region.rs:3`,
`placement.rs:1`, `traversal.rs:1`,
`extent.rs:30`,
`recension/mod.rs:47`, `recension/collation.rs:1`, `recension/batch.rs:1`,
`recension/cycle.rs:1`, `condense.rs:1`, `store.rs:1`,
`wire/mod.rs:1`, `wire/locus.rs:1`,
and the snapshot codec's `wire/snapshot/mod.rs:19`, `wire/snapshot/encode.rs:14`,
`wire/snapshot/pure.rs:20`). It depends on `kairos` for the `Kairos` rank and on
the parent module for `DotSet` (the visible coordinate and the have-set of the wire suffix),
`DotStore` (the axis it implements), `Retired` (the typed condense claim), and
`Metatheses` (the movement record the `recension` read replays, PRD 0022).
== Type inventory
[cols="1,2,3",options="header"]
|===
| Type | Kind | Role
| `Rhapsody` | struct `(skeleton, visible, children, unplaced, woven, thread, visible_pages)` | The sequence store
(`mod.rs:165`):
a grow-only ordering `skeleton`, carried since S194 as the interned `IdentityPlane`
(`identity/mod.rs:307`; the `BTreeMap<Dot, Locus>` form stays the contract
vocabulary), a survivor-law
`visible` `DotSet`, and five derived coordinates, the `children` plane (S116,
coalesced S201), the
`unplaced` placement set (S183), the `woven` recording have-set (S191), the
`thread` positional plane (S200), and the `visible_pages` occupancy plane (S205). Implements
`DotStore` (`store.rs:17`) and carries its own wire frame (`wire/mod.rs:75`).
| `IdentityPlane` | `pub(super)` struct | The skeleton's cost shell (`identity/mod.rs:307`,
crdt-vision arc 11: phase one S194, run-coalesced phase two S199, ruling R-26): per
station, a fiber of 64-slot pages, dense low pages as a prefix vector and far pages
as exceptions (the `DotSet` floor-plus-exceptions precedent applied to layout). A
page `Slot` (four bytes, const-asserted) holds an explicit `RawHandle` into the
contiguous `Locus` column *or* an inline 31-bit rank step: a chain-interior element
(consecutive dot, anchored after its predecessor, rank stepping by the clock) pays
no column entry, its locus materialized on read through the snapshot codec's own
chain law (`chain_step` / `apply_chain_step` from `wire/snapshot/`, the PRD 0023
interlock, so wire runs and memory runs share one derivation). Two structural
bounds keep reads cheap and total: slot zero of a page never steps (a walk back to
an explicit slot stays in-page, at most 63 folds; ascending folds and enumeration
roll the predecessor in `O(1)`), and a step's predecessor slot is always occupied
(removal re-materializes a stepped follower first). `RawHandle` is `Copy + Eq` and
deliberately neither `Ord` nor `Hash` (no read may depend on arrival-order layout)
and never escapes the module. Equality and hashing read the ascending enumeration,
so layout, free-list history, step-versus-explicit spellings, and page residency
stay out of the value; the dual-form agreement pin against the map form is
`prop_plane_agrees_with_the_map_form` (`identity/tests.rs`, chain-append ops
included), with the wire differential
`prop_wire_bytes_are_spelling_independent` beside it in the snapshot suite.
| `ChildPlane` | `pub(super)` struct | The sibling index's cost shell (`children/mod.rs:209`,
crdt-vision arc 11 phase four, S201, ruling R-28): the `BTreeMap<Anchor, Vec<Dot>>`
map form stays the contract vocabulary, and the carried form stores only the
*exceptional* buckets (more than one child; a lone child that is not the chain
child; every `Origin` and `Before` anchor). A chain interior's sole-child bucket is
derived from the identity plane's own entry per read (`chain_child`,
`children/mod.rs:65`, over `IdentityPlane::anchor_of`, constant in the document, a
station-map probe plus page arithmetic: a stepped
slot is anchored `After` its predecessor by the chain law itself), so on honest
traffic the child share is paid per run boundary, not per element. The invariant:
an explicit bucket holds ALL of its anchor's children sorted; no explicit bucket
means no child or exactly the chain child. Reads come back as the `Bucket` view
(`Explicit` slice / `Implicit` singleton) with the double-ended `BucketIter`;
removal reports the stored-tail change (`TailChange`, `children/mod.rs:198`) the
order thread's endpoint forests consume. The dual-form agreement pin is
`prop_child_plane_agrees_with_the_map_form` (`children/tests.rs`).
| `Anchor` | `Copy` enum `Origin \| After(dot) \| Before(dot)` | Where a locus hangs
(`placement.rs:30`, S127): the origin (root region, carrying no dot), the region *after* a dot
(the classic RGA anchor), or the region *before* it (the Fugue left child). The one
meaningless placement, "before the origin", is unrepresentable rather than validated.
`Anchor::dot` (`placement.rs:47`) reads the anchoring dot side-agnostically (`Origin` has none),
which is what the fertility count and the reachability walk read.
| `Locus` | `Copy` struct `(anchor, rank)` | Where one element hangs and how it ranks
(`placement.rs:64`): `anchor: Anchor` (a dot with a side, or the origin, S127) and
`rank: Kairos` (the sibling discriminator, rank *descending*, the kairotic tag riding
inside it).
| `OrderWalk` | fused iterator struct | The lazy in-order walk (`traversal.rs:50`, S183):
the two-frame stack `order` always ran, held as iterator state beside a lazy resume
climb, borrowing the store (mutation under a live walk is a borrow error). Obtained
from `order_walk` (whole document) or `order_walk_after` (resumed mid-document, the
windowed read).
| `OrderThread` | Rhapsody-private struct | The positional plane (`thread/arena.rs`,
crdt-vision arc 11 phase three, S200, ruling R-27): a counted arena tree (parent
pointers, `u32` ids, free list) whose leaves hold walk-contiguous dot-run fragments
(64-slot cap, per-slot visibility mask) and whose nodes cache the `(slots, visible)`
subtree monoids. `thread/arena/mutate.rs` owns point and run mutation;
`thread/arena/reads.rs` owns the root aggregate reads and the indexed
`order_at` / `offset_of` descents. A derived coordinate under the shell
discipline: the walk stays the order's contract form, positions are computed from
the walk's own region rules at `record_locus` (`walk_slot_position`, the bucket-head
and region-boundary arms), the dynamic region boundaries keep region starts and ends
`O(log)` amortized across independent deep seams,
visibility flips ride the merge fold's own residuals, and repaired regions thread
incrementally in walk order. Since arc 11 phase five (S202, ruling R-29) the
region boundaries are run-coalesced (`thread/region.rs`): the ends side
(`SegmentPlane`) never stores a
successor-shaped edge (maximal successor-edged spans are the link-cut forest's
nodes, extents derived from an `O(segments)` break set by range probes; splits and
merges transfer the stored tail edge through `EndpointForest::represented_parent`),
the starts side (`SparseForest`) allocates lazily (`Before` relations only), and
the head invariant (a stored edge always targets a segment head, the one-anchor
argument) keeps contraction sound. The dual-form pin is
`prop_segment_plane_agrees_with_the_per_dot_form` (`thread/region/tests.rs`, against
the S200 per-dot plane kept verbatim as the oracle). Agreement is pinned by
`prop_positional_reads_agree_with_the_order` over every maintenance path. Since
S204 (ruling R-31) the thread also carries the *region splice*, the collation's
fragment-grade re-placement: `extract_range` lifts a slot range out as whole
fragments (boundaries split, the source junction re-coalesced, emptied leaves
retired) into an opaque `Extraction`, and `insert_fragments` splices it back at
the destination (the small splice in place; the bulk splice partitions into
final leaves directly (`thread/arena/splice.rs`), each index entry written
exactly once, both landing
seams re-coalesced; an emptied thread rebuilds bottom-up through
`build_from_fragments`, the bulk tail `from_slots` shares). The splice's own law
is `prop_splice_range_agrees_with_the_slot_model` (the plain slot vector as the
contract form), with the seam pins beside it.
| `OccupancyPlane` | `pub(super)` struct | The visible plane's possession-diff
shell (`possession/mod.rs`, S205, ruling R-32): per `(station, page-of-64)`, one
`u64` occupancy word over the visible `DotSet`, carried as
station-partitioned fibers (per station, its pages ascending, the identity
plane's own idiom; a page birth shifts only its own station's fiber, so no
station's writes move another's rows, the review's cross-station finding)
in canonical form (no zero masks, no empty stations, so equal sets spell
equal planes). Maintained beside every visibility flip: the
`note_visibility` choke point (`weave`, the collation's flip and birth
folds), the in-place merge's expelled/admitted residuals
(`settle_thread_after_merge`), and whole-store builds through `from_plane`
off the crate-internal `DotSet::occupancy_pages` walk (`O(pages +
exceptions)` off the compact form, never a per-dot walk of the prefix).
What the collation's possession mark diffs against: one sorted merge walk
(`changed_pages`), `O(pages)` word compares, each changed page's XOR
yielding exactly the flipped dots, content-exact for any pair (masks are
compared, never counters, so the collation's totality contract narrows
nothing). The dual-form pin is `prop_occupancy_agrees_with_the_set_model`
(in-module), and the plane rides `check_order_thread`, so every structural
sample asserts it against the carried set.
| `OrderWalkRev` | exact-size fused iterator struct | The reverse lazy walk
(`traversal.rs:196`, S200): the visible dots in reverse document order, each step an
`O(log)` thread descent. Obtained from `order_walk_rev` (from the end) or
`order_walk_rev_before` (resumed before a placed slot, the scroll-up window), with
the `is_reachable` refusal boundary the forward resume shares.
| `Verge` | `Copy` enum `Origin \| Before(dot) \| After(dot) \| Terminus` | One sided
span boundary in the identity space (`extent.rs:59`, PRD 0021, S195): the two fixed
document edges plus the slot edges of a woven element, live or tombstone. Extends the
placement `Anchor` by the one boundary placement cannot need (`Terminus`); deliberately
not `Ord` (boundary order is a read against a sequence, never a property of the
vocabulary). The side is the expansion rule: After-start and Before-end expand toward
gap inserts, Before-start and After-end do not, so Peritext's expand flags are the mint's
side choice and no behavior field exists.
| `Extent` | enum `Covered(Vec<Dot>) \| Inverted \| Dangling { start, end }` | The span
projection's total verdict set (`extent.rs:91`): the covered visible dots in document
order (emptiness honest), the crossed ends surfaced, the placeless boundary surfaced per
end. Produced by `Rhapsody::extent` (`extent.rs:163`), which resumes the S183 lazy walk
at the start boundary and scans slots (tombstones included, the slot-level
`next_slot` read the public iterator filters) to the end boundary:
`O(climb + extent)` covered, `O(suffix)` inverted, two placement lookups dangling.
| `Recension` | struct `(performed, ancestry, refused, pending, + collation state)` | The movement
replay read
(`recension/mod.rs`, with maintenance in `recension/collation.rs`, PRD 0022,
S196; maintainable since S203, ruling R-30): a sealed
decision-layer view of the sequence
resolved under a `Metatheses` record. Holds the effective `performed` sequence (a
`Rhapsody` rebuilt from the replayed skeleton) plus the two surfaced verdict lists
(`refused`, refused moves in replay order; `pending`, moves whose target has no birth
here yet). Exposes the sequence reads by delegation (`order`, the lazy walks, `extent`,
placement and visibility) and deliberately no path back to a mergeable store and no
witness read, so the derived reading cannot masquerade as record state. Produced by
`Rhapsody::recension`: births applied first (canonical, never
refused), then `O(M log M)` to order the moves, one `from_parts` rebuild. Since S203
also *maintained*: `Recension::collate(&Rhapsody, &Metatheses)` diffs retained
possession marks against the pair (births fold through `record_locus`, visibility
through slot flips) and replays move-record changes by undo-redo suffix mechanics
over the retained play log (per applied play, the displaced locus), each
re-placement through `Rhapsody::re_place` (`reparent.rs`): since S204 (ruling R-31)
the placed-to-placed transition, every applied replay of a live move, is
`splice_region`, fragment-grade (the region's slots move through the order
thread as whole fragments and the endpoint planes keep every interior edge,
segments being dot-space state; only the two boundary edges move), while the
parking and repair transitions keep the excision protocol's detach order plus
`record_locus`'s placement transition. Verdict sensitivity to unborn dots is
recorded at locus-fold time in the `dangling` map (fold-time recording is complete
where walk-time recording provably is not, since the near-linearity guard skips
walks); every collation is capped at one eager replay (the parity cap), and a
shrunken skeleton (condense) rebuilds. Since S231 (ruling R-49), `ancestry` is
the sole owned exact side-free parent coordinate. Eager ready replay,
maintained collation, and movement batches share it; lawful unplaced history
uses the bounded parent walk until incremental park/repair restores readiness.
`with_exact_ancestry` and a movement batch lend only borrow-scoped relation
queries. The retained collation state and ancestry coordinate are excluded
from equality: two recensions are equal exactly when performed, refused, and
pending are.
| `RhapsodyDecodeError` | `#[non_exhaustive]` enum | Typed failure of the `Rhapsody` wire
decoder (`wire/error.rs:18`): unknown version, unexpected length, the capacity refusal
(`TooManyLoci`, S199: a declared count past the plane's `2^31 - 2` live-entry ceiling
refuses up front rather than folding truncated), and the canonical-form and
structural violations (`ZeroDot`, `NonAscendingLoci`, `BadAnchorTag`,
`VisibleWithoutLocus`), wrapping `kairos::DecodeError` for a rank and
`HaveSetDecodeError` for the visible suffix. A separate codec from the frames it wraps,
so a separate error. The snapshot error carries the same capacity arm as a
documented multi-gibibyte-input belt (every element is backed by six frame bytes).
|===
`Rhapsody` derives `Clone`, `Debug`, `Default` but hand-writes `PartialEq` / `Eq` /
`Hash` (`mod.rs:139`) over the two carried coordinates alone: the `children` index, the
`unplaced` set, the `woven` have-set, and the order thread are pure functions of the
carried state, so two
rhapsodies with equal carried coordinates are equal whether or not either has
materialized them.
Identity is the value, not the accelerations.
== The two coordinates (the pair's asymmetry applied to order)
A collaborative sequence must answer *what survives* and *in what order* under two
different laws, so the store carries two coordinates (PRD 0017's central move):
[horizontal]
skeleton:: the *grow-only* ordering structure, a `Locus` per dot ever woven, carried as
the interned, run-coalesced `IdentityPlane` (`mod.rs:102`, `identity/mod.rs:307`, S194 and
S199; the map form
`BTreeMap<Dot, Locus>` remains `from_parts`'s vocabulary and the decoder's
build form, and point reads materialize by value, so `Rhapsody::locus` returns
`Option<Locus>`). It never shrinks under the normal path
(`weave` and `causal_merge` only add). A deleted element keeps its locus as an *order
tombstone*, because its descendants still anchor through it, which is what lets a
deletion in the middle of a run leave the following text exactly where it was. Only
`condense` (below) ever removes a locus, and only under a typed application claim.
visible:: `DotSet` (`mod.rs:117`), the live elements, governed by the survivor law. It is
exactly the store's `dots()` (`store.rs:16`), the causal coordinate. A dot leaves
visibility only when a removal delta both sides saw supersedes it; a stale peer cannot
resurrect it.
This is the causal pair's own asymmetry (survivors versus everything-ever-seen) applied
to sequencing: survivors ride the `visible` set, and the ordering skeleton is the "never
forgets" side. `is_bottom` (`store.rs:21`) is therefore `visible`-empty *and*
`skeleton`-empty: a fully deleted document (empty visible, non-empty skeleton) is not
bottom, because its skeleton is state a merge must keep.
== The maintained child index (S116; coalesced S201)
A third, *derived* coordinate rides beside the two: `children`, the per-`Anchor` sibling
buckets in `order`'s sibling order (rank descending, dot ascending on ties). Since S127
the key is the `Anchor`, so an `After(d)` bucket and a `Before(d)` bucket are distinct
keys on the one dot; one `sibling_cmp` (`children/mod.rs:51`) sorts every bucket the same
way, both sides. It is a pure function of the skeleton, excluded from equality and
hashing, and never travels on the wire. It exists only to move the `O(n log n)`
grouping-and-sort off the read and onto the write:
* every mutation maintains it incrementally: `weave` inserts the one dot at its sorted
position (`ChildPlane::insert`, `O(log n)` on an explicit bucket, `O(1)` on the
coalesced spelling), `condense` removes an excised dot from its anchor's bucket
(`ChildPlane::remove`, reporting the stored-tail change the endpoint forests
consume), and the fresh-`Self` paths route through `from_parts` (`mod.rs:212`),
which materializes it once through `ChildPlane::build`.
* `order` (`traversal.rs:288`) then merely walks the already-sorted buckets, `O(n)`.
Since arc 11 phase four (S201) the `BTreeMap<Anchor, Vec<Dot>>` map form is the
*contract vocabulary* and the carried form is the coalesced `ChildPlane`
(`children/mod.rs:209`): only exceptional buckets are stored (more than one child; a lone
child that is not the chain child; every `Origin` and `Before` bucket), and a chain
interior's sole-child bucket is derived from the identity plane's own entry per read
(`chain_child`, `children/mod.rs:65`, riding `IdentityPlane::anchor_of`, constant in the
document, a station-map probe plus page arithmetic: a stepped slot is anchored `After`
its predecessor by the chain law itself). One
representation invariant carries every read: an explicit bucket holds ALL of its
anchor's children sorted, and an anchor with no explicit bucket has no child or exactly
its chain child. Inserting a sibling beside an incumbent implicit child materializes
the incumbent first; a removal whose sole survivor is the chain child de-materializes
the bucket; the chain-child probe takes the successor through `checked_add`, so the
`u64::MAX` dot ceiling is a refusal, never an overflow. The dual-form agreement pin is
`prop_child_plane_agrees_with_the_map_form` (`children/tests.rs`), which drives
every consumer read (contents, head, tail, point, suffix, prefix, position, absent
anchors, the endpoint enumeration) against the grouped-and-sorted map form per op.
The store keeps no interior mutability, so the acceleration lives on the `&mut` write path
and the shared-borrow `order` reads it (the maintainers' C8 constraint). This is the
measured per-keystroke pressure the studio probe flagged.
NOTE: PRD 0017 R7 still describes `order` as building a "per-call child index" at
`O(n log n)` per call; that wording predates the S116 maintained index. The behavior of
record is this note and the code: the index is maintained, so `order` is `O(n)` and the
sort is amortized onto the mutations.
== The maintained placement set (S183)
A fourth derived coordinate, `unplaced` (`mod.rs:132`, a `BTreeSet<Dot>`), applies the
S116 move to *reachability*: the woven dots whose anchor chain does not currently reach
the origin (dangling deltas before their repair merge). It exists because the anchor
chain of a forward-typed document is as deep as the document, so a per-read chain walk
would cost `O(depth)` exactly where the windowed read needs `O(log n)`:
`is_reachable` and `order_walk_after`'s resume verdict are both two set lookups against
it. Maintenance mirrors the child index:
* `record_locus` (`maintenance.rs:451`) decides the fresh dot's placement locally off its
anchor's own placement (the chain verdict is inductive, so no walk), parks a dangling
dot in `unplaced`, and on a placed weave runs `repair_placement_from` (`maintenance.rs:926`),
the iterative worklist that re-places the dangling subtree that was waiting on the
new locus (each repaired dot leaves the set exactly once, so the sweep costs
`O(repaired log document)` over the tree and set operations; the common weave costs
two empty bucket probes).
* `condense` drops an excised dot from the set (`condense.rs:131`); sterility means
nothing anchors to the excised dot, so no other dot's placement can change there.
* the fresh-`Self` paths materialize it once in `from_parts` through `build_unplaced`
(`maintenance.rs:162`), the structural walk from the origin over both side buckets: whatever
the walk cannot reach is dangling. A crafted mutual-anchor cycle is simply never
reached, so no walk anywhere needs a cycle guard.
Like the child index it is a pure function of the skeleton, excluded from equality and
hashing, and never travels.
== The maintained recording have-set (S191)
A fifth derived coordinate, `woven` (`mod.rs:140`, a `DotSet`), keeps the skeleton's key
set in compact have-set form: the recording-plane twin of `visible`. It exists because
the witnessed owed read (crdt-vision arc 10, ruling R-21) hands this set to a peer per
anti-entropy probe as the *recording-possession witness*, and folding the skeleton's
keys per probe would re-pay the O(document) cost the read exists to remove. Maintenance
mirrors the other accelerations: `record_locus` inserts the fresh dot (`maintenance.rs:451`),
`condense` removes an excised one (`condense.rs:136`, so a condensed replica stops
claiming what it can no longer serve), and `from_parts` materializes it once from the
skeleton keys (`mod.rs:236`). Its read is `woven()` (`mod.rs:289`), possession claimed
from the maintained coordinate so the witness cannot over-claim by construction; the
witnessed selection itself is `novel_to_witnessed` (`store.rs:126`), the skeleton chosen
by the residual `woven \ recording`, and `support()` (`store.rs:119`) hands the delta
framing the visible set as the maintained survivor have-set. Like the others it is a
pure function of the skeleton, excluded from equality and hashing, and never travels
as state (what travels is the *read*, handed to peers as a claim).
== Reading the order
[horizontal]
order:: `order()` (`traversal.rs:211`) is the document order: an *iterative in-order* walk from
the origin over an explicit two-frame stack (`Frame::Visit` / `Frame::Emit`, `traversal.rs:11`).
For each node it emits, in order, its `Before`-subtrees, then the node itself, then its
`After`-subtrees (S127). Within a bucket the sibling order is one comparator (rank
descending, dot ascending on ties); an `After` bucket is read in stored order and a
`Before` bucket read *reversed*, so both sides obey the one *adjacency law*: a rank above
every incumbent in a bucket lands the element adjacent to its anchor (first after it, or
last before it). This gives insert-before the same subtree isolation insert-after has, so
a backward run stays a contiguous block. It yields *visible* dots and descends through
invisible (tombstone) skeleton. It is iterative over the stack, never recursive, because
skeleton depth is attacker-controllable (a million-deep single-child chain would blow a
recursive stack); each dot gets one `Visit` and one `Emit`, so the walk is `O(n)`. It
returns a `Vec`, the whole-document convenience: since S183 it is exactly
`order_walk().collect()`, one walk implementation behind both reads.
order_walk / order_walk_after:: The windowed order read (S183, ruling R-15, crdt-vision
arc 9). `order_walk()` (`traversal.rs:224`) hands the same walk out lazily as an
`OrderWalk`; `order_walk_after(station, dot)` (`traversal.rs:289`) resumes it
immediately after a placed element, live or order tombstone (a tombstone keeps its
slot; its own emit is skipped), so a viewport consumer pays `O(log n)` to resume plus
the window it takes, not the document. It refuses (`None`) a dot with no place in the
current order (never woven, or dangling before its repair), the `is_reachable`
boundary: fabricating an empty suffix would read an out-of-order delta as "at the
document end". Two mechanisms carry the cost contract: the placement verdict reads the
maintained placement set (above), and the ancestor levels above the resume point are
scheduled *lazily* (`climb_one_level`, `traversal.rs:73`): each level's later-sibling
frames (plus, for a `Before` link, the anchor's own emit and its `After` bucket) join
the stack only when the frames below run dry, each level one bucket lookup plus an
`O(log bucket)` `sibling_position` search (`traversal.rs:247`), so a window that ends
inside the resume point's subtree (a forward-typed document is one such subtree) never
climbs at all. The law is suffix agreement (PRD 0017 R12), property-pinned; the
measured numbers and the terminal-drain residual live in the bench README and PRD
0017's open questions.
children_of:: `children_of(anchor)` (`traversal.rs:391`) reads the maintained index for one
`Anchor`'s siblings in *stored* order (rank descending, dot ascending on ties), `O(1)` to
the bucket, for *both* sides. It yields visible dots *and* order tombstones alike (it
mirrors the skeleton, not visibility), which is what the placement rule needs: a new
sibling's rank must beat every *current* child, live or deleted, because a tombstone still
occupies its sibling slot. The head of the iterator is always the rank to beat: for an
`After` bucket stored order is read order, so the head reads right after the anchor; for a
`Before` bucket `order` reads the bucket reversed, so the stored head still reads adjacent
(right before the anchor) though it is the last of the before-region siblings. The
head-is-the-rank-to-beat invariant holds uniformly on both sides.
anchor_for_visual_insert:: `anchor_for_visual_insert(after)` (`traversal.rs:349`) names the
`Anchor` that lands a fresh top-rank element immediately after the visible element
`after` (`None` at the document start). It carries the Fugue placement rule (S127): the
`base` is `After(a)` when `after == Some(a)`, else `Origin`; if the `base` bucket is
empty (tombstones included) it returns `base` (a top rank there reads right after the
caret); otherwise the caret's in-order successor `s` already lives in that subtree region,
so it returns `Before(s)`, `s` found by an iterative descent (the `base` bucket's
traversal head, then down each `Before` chain, reading a `Before` bucket's traversal head
off its stored *last*). Choosing `Before(s)` over a top-rank `After(a)` is the whole
slice: both place correctly today, but only the Fugue choice groups a backward run into
its own subtree, so two concurrent backward runs cannot interleave. The rank half is
still the caller's, minted strictly above `children_of` (the returned bucket). Its value
is the *seam* the anchoring note reserved for exactly this refinement: callers are
untouched. See
xref:../../../docs/metis-rhapsody-anchoring.adoc[the anchoring note]: the naive editor's
"catX" surprise was a rank bug (a fresh mint does not automatically outrank a sibling a
concurrent peer wove earlier in physical time), not an anchor bug; the sided anchor closes
the backward-run interleaving that note's S127 addendum sharpened from adversarial to
honest ranks.
is_reachable:: `is_reachable(station, dot)` (`traversal.rs:418`) answers whether the
dot's anchor chain reaches the origin through present loci: the dangling-weave
diagnostic, so a caller can tell an out-of-order delta from a placed element (to hold
it back from display) without a full `order` diff. Since S183 the verdict is two set
lookups against the maintained placement set, `O(log n)`; the chain walk it originally
ran happens once per dangling episode on the write path instead of per read. `false`
for a never-woven dot and for the non-dot `0`.
`locus` (`mod.rs:302`), `is_visible` (`mod.rs:308`), `visible_len` (`mod.rs:314`), and
`skeleton_len` (`mod.rs:321`) are the direct-lookup reads; `woven` (`mod.rs:289`) is the
recording have-set (S191, above).
== Weaving (`weave`)
`weave(dot, locus)` (`maintenance.rs:194`) records one element: its locus enters the skeleton and
its dot becomes visible; it returns whether it was recorded. It refuses (no change) a dot
already woven (a dot names one write, `DotStore` law 3, content is never reassigned) and
the non-dot `0`. It *accepts* a dangling anchor (a `(station, dot)` not yet woven here):
the element stays unreachable in `order` until the anchor's locus arrives by a later
merge. This is how out-of-order delta arrival is tolerated; the holdback discipline that
avoids showing a gap lives one layer down in the caller. The skeleton insert must precede
the child-index insert, because `sibling_cmp` (`mod.rs:263`) reads the just-inserted
locus; the placement bookkeeping (park or repair, the placement-set section above) runs
last, off the completed index.
== Weaving a run (`weave_run`, S211 / ruling R-33)
`weave_run(first_dot, anchor, &KairosRun)` is the bulk-ingest write, R-19's
run door fired by the S210 paste number: the head at the caller's anchor
carrying the reservation's first rank, each interior anchored `After` its
predecessor with the successor rank (derived by `wire::apply_chain_step`
at step zero, the codec's own law, so the loci ARE the reservation's
members by the proven fold agreement). All-or-nothing: the identity
plane's `insert_run` is the one freshness, ceiling, and cap authority, and
a refusal moves nothing. The bulk path writes each plane at run grade:
* the identity plane fills pages slot-wise (`identity/mod.rs`, `insert_run`:
interiors as inline steps, page-boundary slots and the head explicit,
the same spelling the per-dot fold produces);
* only the head enters a sibling bucket: each interior is its
predecessor's *derivable chain child*, exactly the relation the
coalesced child plane refuses to store (S201), so the bulk skip is the
invariant rather than an optimization;
* the placement verdict is decided once (interiors stand or park with the
head; an anchor pointing into the run itself parks it, the per-dot
self-reference refusal writ large);
* a placed run enters the order thread as whole fragments
(`thread/arena.rs`, `insert_run` through the S204 splice carrier) and the region
plane as ONE segment (`insert_region_run`: a chain's interior ends
edges are successor-shaped, never stored), with the head's parent edge
registered exactly as the per-dot tail arm registers it;
* the have-sets and the occupancy plane take range writes
(`DotSet::insert_run`, `OccupancyPlane::set_run`).
The one contested corner, a parked dot already waiting on one of the
run's own dots, degrades to the per-dot path so the repair protocol runs
unchanged; honest bulk shapes pay one emptiness read for the check. The
in-place merge's skeleton fold (`store.rs`, `causal_merge_from`) groups an
incoming enumeration into maximal novel chain runs and absorbs each
through `absorb_novel_run` (the same machinery, threading invisible, the
survivor fold's settle flipping what it admits in contiguous runs through
`OrderThread::set_visible_run`), so a shipped paste delta lands at run
grade on the receive side too. The agreement laws live in
`tests/rhapsody/properties/run_grade.rs` (bulk equals per-dot on every
read; the folded run delta equals the pure merge) with the refusal,
parking, degrade, and coalescing pins in `tests/rhapsody/examples/run.rs`.
== Condensation (`condense`, the typed excision)
`condense(&Retired)` (`condense.rs:67`) is the *only* path that shrinks the grow-only
skeleton. It excises every dot that is (a) invisible here, (b) named by the `Retired`
witness, and (c) *sterile* (no locus anchors to it), applied transitively (a dead
unbranched chain is excised tip-first until a survivor, a non-retired dot, or an anchored
dot stops it), and returns how many loci it removed. Sterility is *side-agnostic* (S127):
a dot is fertile if *any* locus anchors to it, `Before` or `After`, so the count reads
`Anchor::dot` and a tombstone with `Before`-children is fertile. Sterility is decided
without recursion: one pass builds an `anchored_by` count map, a worklist excises each
sterile qualifier and decrements its anchor's count, enqueueing that anchor when it falls
sterile, `O(n log n)` per call.
The claim is *typed* because over-claiming is unrecoverable. 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: *stranded text*, invisible in `order`, the unsafe
direction (under-claiming merely retains skeleton, the safe direction). 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 the deployment can gather.
So minerva supplies the mechanism and the caller supplies the claim through a
xref:../mod.adoc[`Retirement`] meet (`../retirement/mod.rs:60`) or the audited `Retired::trust`
escape (`../retirement/retired.rs:77`), the same standing-claims posture as `Stability::report`'s
unverifiable cut (PRD 0011 R8). A bare `DotSet` can no longer reach this path: the
`Retired` witness is the difference between "removed locally" and "removed and applied
everywhere." A visible dot is never excised even when named (visible contradicts
removed-everywhere, so the claim is wrong for that dot and the mechanism declines it
silently). Condensation is *local hygiene, not protocol*: a merge with an uncondensed peer
re-learns excised loci (the union is grow-only), the survivor law keeps the dot invisible,
and a repeat `condense` re-excises; `order` is invariant under the whole cycle.
== The `DotStore` instance
`impl DotStore for Rhapsody` (`store.rs:15`) makes the sequence store a peer of `DotSet`
and `DotMap` on the open axis:
[horizontal]
dots:: `dots` (`store.rs:16`) is the *visible* set: the causal coordinate the survivor law
governs. The skeleton is ordering state, not causal support, so it is deliberately not
part of `dots`.
merge:: `causal_merge` (`store.rs:25`) unions the two skeletons (keeping either side's
locus for a dot both carry, equal by the honest basis, law 3) and folds `visible` by the
survivor law under the two pair contexts. The merged skeleton materializes its child
index once through `from_parts`, a whole-skeleton clone plus full rebuild per fold, which the
S181 scale probe measured linear in the document per composed keystroke; the hot write
paths therefore run `causal_merge_from` (`store.rs:45`, S182, ruling R-14): the same
merge as edits against `self`, each novel locus through the incremental `record_locus`
insertion `weave` uses and the visible fold in place, agreement with the pure form
property-pinned (`prop_rhapsody_merge_from_agrees_with_merge`).
base change:: `restrict` (`store.rs:61`) selects fibers on *both* coordinates and commutes
with `causal_merge` (PRD 0013 R2); it can strand a descendant whose anchor's station is
dropped, so an order verdict on a restriction is *roster-scoped*, not global, the same
created-order hazard the have-set's `restrict` carries. `novel_to` (`store.rs:148`)
selects coverage on the *survivor* coordinate only and ships the skeleton whole
(corrected S190): a peer context covering a woven dot proves the dot was superseded,
never that the peer ever held its locus (a pure-context retract delta conveys coverage
bare, and can outrun the weave delta that carries the place), and a missing tombstone
locus strands every later element anchored to it; the covered-loci filter this replaced
is the counterexample `test_owed_delta_heals_a_tombstone_the_retract_outran` pins, the
S113 `delta_for` unsoundness one coordinate over. The whole-skeleton fragment's cost
fired arc 10 on its instrument (S191): the cure is the witnessed sibling
`novel_to_witnessed` (`store.rs:126`, above), where possession claimed by the peer's own
`woven` read licenses the sub-selection coverage could not, and the bare read keeps its
whole-plane contract for peers that state no witness.
== Wire encoding (PRD 0017 / S117; v2 sided anchor, PRD 0018 / S127)
The Rhapsody carries its own canonical, versioned byte frame (`wire.rs`), a sibling codec
in its own version space alongside the have-set (PRD 0016), vector (PRD 0007), and
`Kairos` (PRD 0002) frames. It is the serialization-and-content-addressing path, distinct
from the `Dotted<Rhapsody>` convergence path.
[horizontal]
encode:: `to_bytes` (`wire/mod.rs:69`) writes `[version=0x02][u32 locus_count]`, then the
skeleton loci in strictly ascending woven-dot order (each `[station: u32][index: u64]`,
a one-byte anchor tag `0x00` origin carrying nothing more / `0x01` after / `0x02` before,
the after and before tags each followed by their `[station: u32][index: u64]` anchor
dot, then the 17-byte `Kairos` rank frame), then the *visible* set as its own have-set
frame appended whole (self-describing, so no outer length prefix). The Fugue side rides
the tag (S127), so a dot-anchored record is the same width on either side. The rank
reuses `Kairos::to_bytes`, so the stamp codec stays the single source of the rank bytes.
Infallible.
decode:: `from_bytes` (`wire/mod.rs:96`) is `from_prefix` (`wire/mod.rs:170`) plus "the tail must
be empty"; `from_prefix` returns the rhapsody and the unconsumed tail. A decoded rhapsody
rebuilds its child index once through `from_parts` (`wire/mod.rs:244`).
Three properties make it more than a memcpy, mirroring the have-set frame and adding one:
. *Canonical bijection.* Decode validates structure *and* canonical form (loci strictly
ascending; no zero-index dot; a known anchor tag, `0x00` / `0x01` / `0x02`), so it never
fabricates a value the encoder cannot produce; every accepted frame re-encodes
byte-for-byte. The retired v1 header (`0x01`) is rejected as `UnknownVersion` (S127; v1
never shipped, so a v2-only decoder keeps the frame canonical by refusing it rather than
translating). Not a sort key: a rhapsody is only partially ordered and its document order
is a read, not a byte property.
. *A structural cross-coordinate law the byte layout cannot carry.* Every *visible* dot
must have a locus in the skeleton (visibility is a subset of the skeleton by
construction), so a frame whose have-set over-reaches the skeleton is rejected
(`VisibleWithoutLocus`), because admitting it would leave `order` unable to place a live
element. A byte-count estimate (42 bytes for a dot-anchored locus, either side) cannot
express this; it is a reference between the two coordinates.
. *A dangling anchor is deliberately ACCEPTED, not refused.* A dot anchor (`After` or
`Before`) naming a dot the frame does not carry is a *legal, reachable* value (an
out-of-order weave, or a removal whose testimony outran the anchor's locus), so refusing
it would break the bijection over legal values. `order` already leaves such a subtree
unreachable, and reachability is a read (`is_reachable`), not a wire refusal. The
rhapsody-convergence fuzz rung discovered this reachable state (the S117 finding), which
is why the codec admits it.
*The suffix dot budget is the skeleton's cardinality (S197 gate review).* The visible
suffix is a have-set frame decoded through
`DotSet::from_prefix_with_budget` and `HaveSetDecodeBudget` (public since S242),
and the budget both rhapsody codecs pass is the decoded
skeleton's cardinality, not the byte length: visibility is a subset of the skeleton, so
the structure the loci bytes already paid for bounds the honest set exactly. This cures
the boundary the older byte-length budget carried (a legal visible set dense above a hole,
a deleted low dot under 38 or more live successors, was refused as the codec's own output)
and makes prefix acceptance independent of trailing bytes (a byte budget read through the
tail inflated with it); a hostile over-dense suffix still refuses, one dot past the
skeleton. The *standalone* have-set frame keeps its PRD 0016 byte-length budget unchanged.
Pinned by `test_a_deleted_low_dot_survives_the_suffix_budget` and
`test_prefix_acceptance_is_independent_of_the_tail` (both codecs),
`prop_round_trips_survive_deletion`, and the v2 twin
`test_rhapsody_suffix_budget_is_the_skeleton`.
Allocation is bounded by the input length, never by the declared count: the byte budget is
checked before each locus record (against the per-locus minimum), so a frame claiming
`u32::MAX` loci is rejected in `O(1)`. `RhapsodyDecodeError` (`wire/error.rs:18`) owns its error
rather than reusing either wrapped one, and is `#[non_exhaustive]` so a future version's
failure is additive (ruling R-8). Byte identity is a v2 contract: v2 supersedes the retired
v1 (S127; the sided anchor widened the tag shape, so v1 is a different value shape and is
refused rather than translated), and a future need (a payload field, a compacted rank) is a
*sibling* codec under a new version byte, never an in-place change (the have-set frame's v1
pin, PRD 0016).
== The snapshot frame (PRD 0023 / S197, the run-compressed sibling)
`wire/snapshot/` is the second codec over the same value space, built for the
late-joiner bootstrap where the v2 frame's 42 bytes per dot-anchored locus dominate
(crdt-vision arc 5; ruling R-25). Three files carry the S187 dual-home split:
[horizontal]
`snapshot/pure.rs`:: the *dual-homed validating scan* (the R-18 machinery's second
instance): every structural and canonical check over the run table, the rank-step
columns, the free section, and the merged-order walk, written in the Creusot 0.12
subset, proven total under the detached `proofs/` crate (74 prover certificates,
13 modules), and compiled contract-free by minerva. Flat `Vec<PureLocus>` output;
the map fold stays in the adapter. Also home of the chain law: `chainable` and
`rank_successor` (the clock fold's send-step successor; agreement with
`fold::advance` is Kani-proven, `snapshot_rank_step_matches_the_clock_fold`).
`snapshot/encode.rs`:: the greedy maximal-chain factoring and emission, sharing
`chainable` verbatim with the decoder so the factoring is the value's only
spelling (the bijection argument lives in PRD 0023).
`snapshot/mod.rs`:: the thin adapter: `to_snapshot_bytes` flattens the skeleton's
ascending enumeration and appends the visible have-set frame;
`from_snapshot_prefix` lifts the core error, folds the flat loci through
`from_parts`, and re-checks the visible-subset law exactly as v2 does;
`SnapshotDecodeError` (`snapshot/error.rs`) owns the refusal vocabulary, including
the canonicality arms v2 has no analogue for (`SplitChain`,
`NonCanonicalRankStep`, `RunTooShort`, `NonCanonicalOriginAnchor`). Since S199 it
also exports the in-memory door to the chain law, `chain_step` /
`apply_chain_step` (`pub(in ...rhapsody)`), which the run-coalesced identity
plane stores and materializes its inline steps through: one derivation for wire
runs and memory runs, the PRD 0023 interlock discharged.
A chain run (consecutive dots of one station, each anchored AFTER its predecessor,
kairotic and minting station constant, rank stepping by the clock successor or a
positive sub-`2^48` physical advance) costs one 46-byte fixed-width row plus six
bytes per interior element, against 42 each in v2: the honest two-author 65k
document lands at 434,222 bytes against 2,752,542 (6.3x, exact, probe-asserted in
`scale.rs`), single-author near the 7x asymptote. Deletion never moves the
factoring (visibility is the suffix's business, `test_tombstones_ride_inside_runs`).
The dangling-anchor acceptance, the visible-subset refusal, and the have-set dot
budget carry over from v2 verbatim; expansion is additionally bounded because every
materialized element is backed by at least six frame bytes. Test map:
`src/metis/tests/wire/rhapsody/snapshot/` (round trips honest and adversarial, the
v2 agreement, the compression accounting, the successor twins, the shaped
refusals, and `prop_wire_bytes_are_spelling_independent`, the S199 dual-form
differential: a condense-churned plane and its decode rebuilt twin spell identical
bytes on both codecs) plus the `rhapsody_snapshot_from_bytes` fuzz target and the
`snapshot_encode` / `snapshot_decode` bench points.
== Notes for a future editor
. *The derived coordinates stay maintained, not rebuilt.* Every mutation path
(`weave`, `causal_merge`, `causal_merge_from`, `condense`, `from_parts`) must leave
every `children` bucket read equal to the map form's (`ChildPlane::build`'s
grouped-and-sorted vocabulary; spelling may drift, reads may not), `unplaced` equal
to `build_unplaced(&skeleton, &children)`, and the order `thread` equal to a rebuild
from the walk, including its dynamic region endpoints. Repairs thread their
contiguous regions directly; condense replaces the affected last-child edge before
retiring a sterile endpoint node. All are excluded from equality and hashing,
so a stale one is a *silent* read bug the value comparison will not catch;
`prop_cached_order_agrees_with_naive_on_every_replica`,
`prop_children_of_agrees_with_the_sibling_order`,
`prop_child_plane_agrees_with_the_map_form` (in-module: every bucket read against
the contract form per op),
`prop_order_walk_after_agrees_with_order_suffix` (whose `is_reachable`-coincidence
assertion pins the placement set against the oracle), and
`prop_positional_reads_agree_with_the_order` (whose arms cover every maintenance
path) are the guard. Do not add
interior mutability to rebuild any of them lazily in a read (the C8 constraint: the
reads take `&self`).
. *Every skeleton walk is iterative.* `order`, the `OrderWalk` stack and its lazy climb,
`repair_placement_from`, `build_unplaced`, and `condense` all avoid
recursion because skeleton depth is attacker-controllable. A change that reintroduces
recursion over the skeleton reopens the stack-exhaustion hole R7 closed.
. *Deletion is causal invisibility, never structural removal.* Only `condense` removes a
locus, and only under the `Retired` claim. An over-claim strands text (the unrecoverable
direction); the type is the guard, and the visible check is the belt.
. *The wire codec accepts a dangling anchor and enforces visible-subset-of-skeleton.* These
are the two halves of "serialize exactly the legal values": do not add a dangling-anchor
refusal (it would break the bijection over reachable states), and do not drop the
`VisibleWithoutLocus` check (it admits a value `order` cannot place).
. *The recension is a derived read, never a store (PRD 0022).* `recension` rebuilds an
effective `Rhapsody` through `from_parts` and hands it back inside the sealed `Recension`
(reads by delegation, no store exit, no witness read). Do not add a path from `Recension`
back to a mergeable value or expose its `performed` field: the
production-recording-decision rule is what keeps the chosen reading from masquerading as
the record. Births are canonical: the skeleton is a forest, so `recension` applies every
birth first, unconditionally, and only a *move* is ever refused, leaving its target at its
prior placement. Keep it that way: a refused birth would detach visible content (the P2 a
move ranked below its anchor's birth once exposed), so the walk must stay confined to
moves and the visible plane must stay the store's own, untouched.
. *Exact ancestry has one owner and one mutation boundary (S231).* `Recension`
owns the coordinate; records, equality, wire state, and consumers do not.
Every effective-locus replacement updates identity and ancestry together.
A batch transfers the same coordinate and returns it on explicit or panic
finalization. Reverse suffix restoration performs no relation query; a
tentative suffix that remains unplaced restores the exact pre-call state and
composes no testimony. Unknown and unplaced total-replay shapes retain the
bounded parent-walk semantics.
. *The collation records verdict sensitivity at the fold, never at the walk (S203).* Any
locus folded into a replay whose anchor is unborn records that reference in the
`dangling` map (a birth records the whole log; a play application records its own
key). Do not move this recording into the cycle walk: the near-linearity guard skips
exactly some of the walks a later birth can flip, so walk-time recording is
provably incomplete (the collation property's first counterexample, and the five
mutation-verified pins in `tests/metathesis/collation/`). `Rhapsody::re_place` is
`pub`-less replay machinery for the collation alone: the record's own write paths
must never reach it (a recorded locus is testimony, minted once), and its caller
owns acyclicity (the verdict precedes every application, and an unwind restores a
locus that was once lawfully applied).
== The re-foundation fold (`refound`, PRD 0024 stage one)
`refound(&self, moves: &Metatheses) -> Result<Refounded, UnsealedStratum>`
(`refound/mod.rs`) is the epoch charter's pure fold: the recension bakes
into placement, live elements re-mint per original station in walk order
(the `OrderWalk` contract makes the fold's input exactly the effective
live order), interiors spell through `wire::apply_chain_step` at step zero
so the new store is born coalesced and its recording have-set
floor-perfect, and ranks come from a fixed per-station base, never a live
clock (same stratum, same fold, same bytes at every replica). `Refounded`
carries the new store plus the frozen `RefoundMap` (live-at-cut compaction
below each station's ceiling, the affine shift above it, `None` for a
swept tombstone); `UnsealedStratum` refuses the one input a witnessed cut
could not have produced (an unplaced woven dot or a pending movement). The
declaration, adoption, seal, and shadow are deliberately absent: stage
two's territory.
Beside it since S263 (ruling R-50) sits the seal consignment's store half,
`Recension::consign_store(&self, &RefoundMap)` (same module,
`pub(in crate::metis)`): the same spelling applied to the *final* reading
through the *frozen* map rather than a fresh re-mint, in
tombstone-inclusive slot order (`OrderThread::slots`, a streaming walk
buffering one leaf, added for exactly this caller). It carries
window-deleted cut-live images as order tombstones, skips window-born-dead
and swept identities, and checks successor adjacency with checked
arithmetic before spelling a chain step (a lawful affine image can sit at
`u64::MAX`; the frozen map does not renumber this walk, so adjacency is
tested, never assumed). The recension stays a sealed view publicly: the
reading crosses back into record state only through the epoch seal's
witnessed door, `EpochShadow::consign` (the metis note's stage-four
section owns that contract).
The R2 proof plan is fully discharged (S217), split per ruling R-9. The
affine arithmetic is Kani-proven
(`the_affine_shift_is_sound_over_the_sealed_bounds`, in-module). The
identity arithmetic (station `s`'s `k`-th walk element mints `(s, k)`) is
the *third dual-homed Creusot core*, `refound/pure.rs`: the shipped fold
calls `pure::remint` and spells loci over its output, so the proven code
is the running code. Its contracts are total correctness under
`#[check(terminates)]`, index-aligned totality, station preservation,
per-station order preservation, injectivity (the live-content bijection),
same-station consecutiveness (which licenses the fold's inline chain step
to test only the walk predecessor's station; the head-grade spelling is
pinned in `tests/refound.rs`), and floor-perfection in predecessor form
(counters predecessor-closed, tallies attained, coverage bounded; exactly
`1..=n_s` by descending induction, the expanded form staying sampled in
`assert_fold_laws`). The predecessor form is deliberate: a `forall k`
bound only by arithmetic gives E-matching no term to instantiate, so the
direct `1..=n_s` quantifier is unprovable-in-practice while each one-step
witness transfer discharges in seconds; the lesson is recorded in
`proofs/README.adoc`. A private `BTreeMap<u32, usize>` indexes the
proof-facing tally vector, keeping arbitrary-station lookup logarithmic;
`StationTallies` owns both forms behind an explicit Creusot type invariant,
and its `mint` transition is the narrow trusted collection contract because
Creusot 0.12 does not model `alloc::collections::BTreeMap`. The large distinct-
station regression guards against restoring the quadratic scan.
Since S278 (ruling R-60) the map has its canonical wire form,
`refound/wire/`: `RefoundMap::to_bytes` / `from_bytes` /
`from_bytes_with_budget` under `REFOUND_MAP_WIRE_V1`, one row per
ceiling station carrying the station, the cut ceiling, the live count,
and the old-epoch indices whose one-based position *is* the new index
(so station preservation and the `1..=n_s` image, the proven contracts
above, are unrepresentable to violate on the wire, and entry order
carries the walk-order permutation as semantic content). Refusals are
layered (`RefoundMapDecodeError`), the two-ceiling
`RefoundMapDecodeBudget` (station rows, cumulative entries) sits
beside the input-length default, and the suite lives in
`../tests/wire/refound_map/` with the `refound_map_from_bytes` fuzz
target beside it. Minted as the S274 lineage recipe's byte carrier;
the digest over these bytes stays outside the `no_std` core.
== Test map
Tests live under `../tests/rhapsody/` (store behavior), `../tests/rhapsody_convergence/`
(the op-tape semantic twin), `../tests/wire/rhapsody/` (the frame), and `../tests/studio/`
(the editor-shaped sessions), all `no_std`-clean. The invariant-to-test mappings are in
xref:../../../docs/prd/0017-metis-rhapsody-sequence-store.adoc#_invariants_and_their_tests[PRD 0017]
and, for the sided anchor,
xref:../../../docs/prd/0018-metis-rhapsody-sided-anchor.adoc#_invariants_and_their_tests[PRD 0018].
Strong-list specification tests (S288, ruling R-70): `../tests/strong_list/`
carries the implementation-blind order ledger (every observed visible order
contributes its adjacent pairs; the verdict is one witness total order or a
constraint cycle with per-step observation provenance) and its falsifier
exhibits (the pair flip, the rotation every pairwise view passes, the
real-execution witness embedding, and the block-interleaving pass that keeps
PRD 0018 R6's FugueMax corner a residual). Both convergence tape twins feed
the ledger every post-op, post-gossip, condense, read, and converged order
and demand the verdict at convergence, beside the per-weave index-insertion
translation law (the parent-with-side to insert-at-position deliverable);
`../tests/refound.rs` composes the oracle across the epoch boundary through
the frozen rename map (both lanes: insert/delete, and a moved stratum whose
pre-seal ledger observes only the baked effective order, movement being
outside the specification).
Chain-identity tests (S212): `../tests/rhapsody/properties/chain_identity.rs`
carries the invariant's end-to-end law
(`prop_chain_identity_survives_interior_ambiguity`: run-bearing histories,
an interior-edit storm of chain splits, span deletes, and undo retracts,
a concurrent fork converged through both merge forms, then locus
preservation for every ever-woven dot, exact relative order of surviving
originals, and byte-canonical round trips through both codecs);
`wire/snapshot/proofs.rs` carries the chain-law Kani harnesses
(`chain_step_spelling_is_lossless`,
`a_committed_send_succession_always_chains`); and
`../tests/metathesis/foundations.rs` carries the replay-foundations pins
(the fixed-point-not-optimum three-move counterexample and the
per-stream non-composability triangle). The ladder these rungs form is
documented in the shell-discipline note's chain-identity section.
Run-grade tests (S211, ruling R-33): `../tests/rhapsody/properties/run_grade.rs`
carries the two agreement laws (`prop_weave_run_agrees_with_the_per_dot_weave`, every
positional, visibility, and reachability read compared with thread and occupancy
invariants held; `prop_a_run_delta_absorbs_like_the_pure_merge`, idempotence
included) beside the fragment-count and one-segment absorb pins, the unaligned
bulk-retract settle pin (position-exact against the walk), and the fold-side
parked-waiter degrade pin; `../tests/rhapsody/examples/run.rs` carries the whole-run
refusals (zero, ceiling, occupied middle, at-the-ceiling lawful), the dangling run
parking whole with direct parked reads, the self-anchored park, the weave-side
degrade, and the byte-identical bulk-versus-per-dot paste. The substrate agreement
properties live in their own modules (`identity/tests.rs`, `possession/tests.rs`,
`thread/arena/tests.rs`, `thread/region/tests.rs`; `../tests/dot_set/properties/exact.rs`), and the standing model's `Paste`
op (`arb_ops_with_paste`) feeds run-woven documents to the convergence, fold,
witnessed, order, and positional suites by construction.
Positional-read tests (S200, arc 11 phase three):
`prop_positional_reads_agree_with_the_order` (the thread's one law, agreement, over
histories enriched with sided anchors and tombstones: length, selection, offsets,
both reverse walks, and the refusals against `order()` and the independent oracle,
checked on the converged rebuild, the in-place fold seeded from a POPULATED replica
so the merge settle's expelled-flip arm runs under the oracle (the S200 review's
coverage finding; the from-empty fold keeps its own arm for maximal parks and
repairs), the pure-weave walk-order path where every insert runs the incremental
position rules, and through condense, with the thread's structural invariants
asserted exhaustively in every arm); the deterministic edges land in
`examples/positional.rs` (offset selection, the tombstone slot bound, the reverse
windows, the unplaced refusal and its repair, the lower-rank Before sibling's
region-start arm, offsets through condense, and the review pins:
`test_a_deletion_through_the_in_place_fold_moves_the_offsets`, the expelled-flip
arm's deterministic shape;
`test_a_deep_seam_insert_uses_the_region_endpoint` and
`test_split_deltas_cross_independent_deep_seams`, the maintained endpoint path,
priced by the `deep_seam_merge`, `deep_seam_merge_split`, and
`deep_seam_merge_scattered` bench points; and
`test_a_self_anchored_element_is_unplaced_on_every_path`, the S200 P1's
placement fix on the weave and decode-merge paths; and
`test_a_repaired_region_threads_in_walk_order`, the incremental repair path over
both anchor sides); and the
`thread/arena/tests.rs` suite
pins the structure itself (coalescing, splits, rebase and re-home on removal,
level growth, bulk-versus-incremental agreement, the `nth_set_bit` select, the
ceiling-fragment refusal, and fragment-grade splice seams). Region endpoint
representation and old-sibling capture remain pinned separately in
`thread/region/tests.rs`.
Child-plane tests (S201, arc 11 phase four, `children/tests.rs`):
`prop_child_plane_agrees_with_the_map_form` (the shell's one law, agreement: over op
tapes run in the production call order, every consumer read, bucket contents, head,
tail, point, suffix and prefix slices, absent anchors, the endpoint enumeration, and
the removal's stored-tail verdict, against the grouped-and-sorted contract form and
a fresh `ChildPlane::build`); the deterministic pins are
`a_chain_stores_no_explicit_bucket` (the coalescing accounting),
`a_second_sibling_materializes_and_departs` (materialize-on-contest and
de-materialize-on-survivor),
`a_ceiling_dot_probes_no_successor` (the `checked_add` refusal at `u64::MAX`),
`an_implicit_child_departs_with_its_plane_entry` (the emptied-bucket tail verdict),
and `a_self_anchored_dot_stores_explicitly`. The facade-level factoring agreement
(explicit children == locus-column runs == thread fragments == wire run count) is
the scale probe's `child_plane_pins` arm.
Region-plane tests (S202/S255, arc 11 phase five, `thread/region/tests.rs`):
`prop_segment_plane_agrees_with_the_per_dot_form` (the shell's one law, agreement:
over protocol-shaped edge tapes, insertions, successor-shaped and explicit edge
replacements on both sides, cuts, and the replace-before-retire excision order, the
segmented plane and the S200 per-dot plane agree on every verdict and every endpoint
read, with the segment invariants checked per op); the deterministic pins are
`a_typed_chain_allocates_no_forest_node` (the hot path is set arithmetic),
`a_mid_chain_split_inherits_the_stored_edge` (the edge-inheritance arm the per-dot
form never needed), `a_ceiling_dot_replaces_without_overflow` (the `checked_add`
refusal at `u64::MAX`), and the S200 old-sibling capture pin
(`region_end_replacement_does_not_capture_the_old_sibling`), passing over the new
plane verbatim. The facade-level pins are the probe's segments-equal-runs and
one-node-per-boundary arms plus the coverage assertion `check_order_thread` runs in
every positional-property arm.
Possession-plane tests (S205, ruling R-32, `possession/tests.rs`):
`prop_occupancy_agrees_with_the_set_model` (the shell's one law, agreement:
over any op tape the maintained plane equals a fresh build from the model
set, and the changed-pages walk between any two snapshots extracts exactly
the symmetric difference), with `a_page_is_born_and_retires_with_its_bits`,
`the_changed_walk_reads_both_directions`, and
`a_ceiling_dot_occupies_the_last_page` beside it. The plane also rides
`check_order_thread` (every structural sample asserts it against the carried
set), `check_collation` pins the mark's exact adoption of the pair's plane
(canonical form included), and `test_a_high_page_flip_collates_exactly`
(`tests/metathesis/collation/`) exercises the bit extraction above page
zero, the arm the small-document generators cannot reach;
`prop_batched_flips_agree_with_the_point_form` (in-module) pins the batched
settles against the point form, and
`test_a_bulk_retirement_collates_exactly` the whole-page-death shape whose
per-row removal the gate review priced quadratic (the
`collate_bulk_retract` bench point carries the number). Fourteen sites are
mutation-verified: the `note_visibility` choke point (whose debug belt, the
plane never LEADS its carried set, is what makes the born-bit hygiene
killable), both settle arms, the `from_plane` build, both batch
applications, `apply_pages`' zero-row retention, its incremental
classifier and tail-push arm (the singleton-delivery regime), the
empty-fiber station retirement, `apply_flips`' staging seed, the floor
partial-page mask, and the bit extraction (killed at both the unit and
integration seams).
Region-splice tests (S204/S256, ruling R-31, `thread/arena/tests.rs`):
`prop_splice_range_agrees_with_the_slot_model` (the splice's one law, agreement:
over arbitrary run layouts and sequences of range moves, extract-then-insert equals
the plain slot-vector contract form on every read, invariants checked per move);
the deterministic pins are `a_range_splice_moves_fragments_wholesale` (an interior
move splits only at the seams), `a_returned_splice_coalesces_back` (a move and its
undo restore the fragment count, masks intact),
`an_extraction_heals_the_junction_it_opens` (the source-junction coalesce),
`a_whole_document_splice_rebuilds` (the emptied-thread bulk rebuild), and
`a_splice_seam_at_the_dot_ceiling_refuses_overflow` (the `checked_add` discipline
at the coalescing probe). The facade-level economics pin is
`test_a_suffix_move_storm_stays_fragment_grade` (`tests/metathesis/collation/`):
a descending-rank storm of whole-suffix moves stays exact and never trips the
eager-parity cap, where the slot-granular charge does (the mutation check). Nine
splice sites are mutation-verified: the work unit, both boundary-edge arms, the
coalesce mask shift, the split tail mask, the extraction's index removal, the
junction coalesce, and the bulk partition's two sites (the fill-room arithmetic
and the chunk attachment, each failing through the leaf-cap invariant
`check_invariants` carries for exactly this).
Store properties: `prop_replicas_converge_to_the_order_oracle` (R1: any history and fold
order converges to a naive order oracle, every replica absorbed),
`prop_order_is_fold_order_independent` and `prop_cached_order_agrees_with_naive_on_every_replica`
(R1 / the maintained index), `prop_skeleton_is_grow_only` (R2),
`prop_visible_is_woven_minus_expelled` (R3), `prop_children_of_agrees_with_the_sibling_order`
(R4, now on *both* sides), `prop_backward_runs_stay_contiguous` (PRD 0018 R3, the sided
anchor's new law: repeated insert-before at a shared boundary reads as a contiguous block
after any merge order), `prop_is_reachable_agrees_with_the_walk_oracle` (R6),
`prop_restrict_commutes_with_merge` (R8),
`prop_order_walk_after_agrees_with_order_suffix` (R12, S183: the windowed walk's suffix
law over histories enriched with sided anchors and tombstones, the refusal law, and the
`is_reachable` coincidence), the condense laws
(`prop_condense_commutes_with_merge`, `prop_condense_under_an_honest_claim_preserves_order`,
`prop_monotone_claim_condense_is_idempotent`), and the visual-insert law
(`prop_visual_insert_round_trips_through_order`).
Store examples pin the named cases: `test_deletion_keeps_order`,
`test_is_bottom_distinguishes_empty_from_fully_deleted`,
`test_chain_reads_in_typing_order` and `test_two_chains_at_the_origin_stay_contiguous` (R5,
the RGA no-internal-interleaving fact for forward runs),
`test_backward_runs_at_the_origin_stay_contiguous` (PRD 0018 R3, the same guarantee gained
for backward runs), `test_sibling_determinism`,
`test_dangling_anchor_is_accepted_but_unreachable` / `test_dangling_then_repaired` (R6),
`test_weave_refuses_duplicate_and_zero`, the `test_walk_*` set (R12, S183: suffix at
every slot, the `take(k)` window, tombstone resume, `Before`-anchor climb, and the
no-place refusal with its repair), the `test_conformance_*` set (R9, the five
`DotStore` laws), the `test_condense_*` family (sterile / transitive / diamond / visible
guard / gossip cycle, and `test_over_claimed_retirement_strands_a_laggards_anchor`, the
typed hazard). The S127 seam examples pin the Fugue placement rule:
`test_anchor_for_visual_insert_returns_the_base_on_an_empty_bucket`,
`test_anchor_for_visual_insert_returns_before_the_successor_on_a_nonempty_bucket`,
`test_anchor_for_visual_insert_descends_a_before_chain_through_a_tombstone` (PRD 0018 R4),
and `test_visual_insert_top_rank_lands_immediately_after_the_caret` (S116, still the
placement invariant); the both-sides `children_of` examples are
`test_children_of_agrees_with_the_order_sibling_bucket` and
`test_children_of_head_is_the_rank_to_beat_on_both_sides` (PRD 0018 R2). The studio
sessions add `test_concurrent_backward_runs_stay_contiguous` (over the editor's
`insert_before_visual` helper), the editor-shaped witness of the backward-run cure. The
op-tape twin (`prop_rhapsody_op_tape_interpreter_matches_the_suite`, S106) replays a
serialized edit tape against the suite's model, the always-on partner of the
`rhapsody_convergence` fuzz target; it grew a `WeaveBefore` op and an in-order
`reference_order` (S127) so the convergence rung actually generates backward runs.
Wire tests (`../tests/wire/rhapsody/`): `prop_rhapsody_bytes_round_trip`,
`prop_rhapsody_bytes_are_canonical`, `prop_rhapsody_decode_then_encode_is_identity`, the
totality trio `prop_rhapsody_from_bytes_never_panics` /
`prop_rhapsody_truncation_never_panics` / `prop_rhapsody_flip_byte_stays_total`,
`prop_rhapsody_dangling_anchor_round_trips` (the accepted-dangling-anchor value survives the
frame), and `prop_rhapsody_dot_anchored_locus_is_42_bytes` (the layout size, the same 42
bytes on either side, S127). Examples pin `test_rhapsody_to_bytes_layout`,
`test_rhapsody_before_anchor_round_trips` (the `0x02` before-tagged locus survives the v2
frame, S127), every rejection variant (`test_rhapsody_rejects_*`: unknown version, the
retired v1 version (`test_rhapsody_rejects_retired_v1_version`, S127), non-ascending loci,
zero-index dot, bad anchor tag, malformed rank, malformed visible suffix,
visible-without-locus), `test_rhapsody_truncation_at_every_boundary`, and
`test_rhapsody_inherits_have_set_dot_budget` (the wrapped `RunTooLong` boundary). The
coverage-guided `fuzz/fuzz_targets/rhapsody_convergence.rs` target drives the semantic
convergence and the never-panic / re-encode invariants past what proptest reaches.
Collation tests (`../tests/metathesis/collation/`, S203, ruling R-30): the maintained
recension's one law is per-event exact agreement with the eager replay,
`prop_collation_agrees_with_the_eager_replay` (a maintained view per replica, collated
after EVERY op of insert/delete/move/undo/gossip histories extended with move-only
gossip, asserted through `Recension::check_collation`: value equality, the whole order,
every positional read, placement and visibility verdicts on every woven dot, and the
thread's structural invariants; bounded generated shapes also validate every
coordinate edge and relation against an independent parent walk after each operation;
the idle collation is asserted a no-op). The
deterministic pins: typing never replays, the out-of-order unwind, the retract restore,
the pending activation, the condense rebuild, the descending-rank storm, the four
birth-sensitivity pins beside `test_a_late_birth_reverdicts_a_walked_verdict` (the
guard-skipped, dangling-weave-behind-the-anchor, and two construction-time shapes), and
the gate review's three (`test_a_replaced_testimony_collates_as_a_replacement`, the
record's content-compare at equal keys;
`test_an_unrelated_text_violates_the_basis_loudly`, the debug belt on the text side's
trait-law-3 contract; `test_a_late_birth_under_a_twice_moved_target_unwinds_safely`,
the P1 phase-order pin: births fold strictly AFTER the unwind, so a historical
displaced locus never restores into a state richer than the one that applied it),
eight sites in all verified by mutation (delete or invert the site, a named test
fails).
Movement replay tests (`../tests/metathesis/`, PRD 0022, S196): the `recension` read is a
`Rhapsody` method but tested beside its `Metatheses` record.
`prop_recension_converges_and_matches_the_reference` (R4: every replica's order, refusals,
and pending set agree with each other and an independent replay oracle over
insert/delete/move/undo/gossip histories, plus the empty-record identity) and
`prop_no_moves_means_no_refusals` (R3) are the laws; the examples pin the flipped
identity-fork exhibit (`test_the_exhibit_flips_a_concurrent_edit_follows_the_move`), the
fixed-rule verdicts (`test_concurrent_moves_of_one_element_resolve_by_rank`,
`test_a_move_cycle_is_refused_deterministically`), undo, the tidy re-move, marks over
moves, and the out-of-order surfaces. The `Metatheses` store's axis laws run in the shared
conformance harness (`prop_metatheses_conforms_to_the_axis`, in
`../tests/causal_store/foreign/laws/axis.rs`).
S231 adds the public exact-relation arms, immediate batch-query visibility, origin
bypass, ancestry admission before callback entry, transactional `UnplacedResult`
rollback with later rank admission, and panic-safe coordinate return to the batch
examples.