= Module: metis
:toc: macro
:toclevels: 2
Design notes for the `metis` module, co-located with `mod.rs`. This is the
implementer's view: what the layer is for, the primitives it ships, and the
invariants a change must not break. Product-level intent lives in
xref:../../docs/prd/0004-metis-causal-ordering.adoc[PRD 0004] (the version vector),
xref:../../docs/prd/0005-metis-causal-order-buffer.adoc[PRD 0005] (the delivery
buffer), and xref:../../docs/prd/0006-metis-event-producer.adoc[PRD 0006] (the event
producer); the wider plan is in xref:../../docs/target_arch/index.adoc[the target
architecture]. The wire encoding for the `VersionVector` and the `Event` envelope is
specified in xref:../../docs/prd/0007-metis-event-wire-encoding.adoc[PRD 0007]
(implemented in S16b) and described in xref:#wire-encoding[its own section]
below. The
*deinotēs* dimension, a caller-defined skill for _resolving_ the concurrent frontier
the buffer linearizes by `Kairos`, is chartered in
xref:../../docs/prd/0008-metis-deinotes-concurrency-resolution.adoc[PRD 0008] (S23a,
held for sign-off _and_ gated on a concrete caller); it carves no `Resolver` seam. The
buffer does expose that frontier read-only (`frontier`, an *antichain*; S25,
xref:#ready-antichain[below]), the caller-owned material such a resolver would consume,
but the resolution policy itself stays the caller's. The buffer's _gate_, the stability rule, is a
caller-parameterized `Gate` seam (xref:../../docs/prd/0009-metis-ideal-gate-generic.adoc[PRD 0009],
implemented in S27b): `Ideal<T, G: Gate>` runs the fixed machine over the gate, with `Causal` (the
happens-before `VersionVector` rule, aliased `CausalIdeal<T>`) and the scalar `Fifo` per-source
watermark (`FifoIdeal<T>`) as the two leaf gates, S237's `And<A, B>` composing two
release-driven rules, and
`Event<T, D>` carrying the gate's dependency *data*. The gate sits below the frontier, the _deinotēs_ resolver above it (still
uncarved). The gate is *named* at every buffer through its alias, never a silent default, so a
future non-causal gate (a retrodictive reading of the same data, say) is a peer of `Causal`, not
awkward beside a privileged default. See xref:#gate-seam[the gate seam] below.
The order-theoretic foundations the layer's vocabulary rests on, why the delivered set is an
*order ideal* (down-set) and the same object as its `VersionVector` (Birkhoff), why `frontier`
is its *cover* (the leading edge, not the trailing `max(I)` or the vacuous spectral boundary),
and which duality governs which regime, are collected in
xref:../../docs/cut-lattice-and-frontier.adoc[the cut-lattice note]. Its dual companion, the
algebraic-geometry reading (the spectrum, the structure sheaf, and the gluing of per-node
sections), is a held horizon in
xref:../../docs/prd/0010-metis-spectrum-algebraic-geometry-horizon.adoc[PRD 0010] (S29a, design
only). That horizon's one buildable signal fired in S78: the cross-node *meet* is carved as the
fourth primitive, `VersionVector::meet` plus the roster-fixed `Stability` tracker whose
`watermark` is the safe-to-forget cut `min_n D_n`, specified in
xref:../../docs/prd/0011-metis-causal-stability-watermark.adoc[PRD 0011] (mechanism only; the
forgetting policy and membership change stay the caller's; see
xref:#stability-tracker[the stability tracker] below).
The sixth primitive is the *causal store algebra*
(xref:../../docs/prd/0015-metis-causal-store-algebra.adoc[PRD 0015], S96, ruling R-12): the
production-side half of the dotted-vector charter. `Dotted<S>` brackets a store of
dot-tagged content with the causal context of every dot ever seen; its `merge`, the pair's
only write, keeps a dot exactly when no side that saw it has dropped it (the *survivor
law*), so removals need no tombstones, removed state cannot resurrect through a stale
peer, and unseen concurrent writes survive concurrent removals. `DotStore` is the layer's
second deliberately open axis (the `Gate` posture): minerva ships the dot-shaped `DotSet`
and `DotMap<K, S>` instances plus the one value-carrying `DotFun<V>` (S102, the multi-value
register shape), while a consumer's own payload store slots in as a caller impl. See
xref:#causal-store[the causal store] below.
The S97-S118 exploration epoch grew that pair into a working substrate, and its smaller
surfaces are documented here beside the primitive they extend; the one large self-contained
subsystem, the `Rhapsody` sequence store, earns its own co-located note
(xref:rhapsody/mod.adoc[`src/metis/rhapsody/mod.adoc`], the sequence instance of the
`DotStore` axis). Documented below: `DotFun<V>`, the in-tree payload store
(xref:#payload-store[below]); `Composer`, the write-side facade over a `Dotted` pair, the
causal-pair analogue of the `Producer` (xref:#composer[below]); `Purview` and `Retirement`,
the roster-fixed gossip-targeting and removal-tracking duals of `Stability`, one carrier
down over `DotSet` contexts (xref:#purview[below], xref:#retirement[below]); `Cut`, a
`VersionVector` witnessed gap-free by construction, which makes the PRD 0011 R8 cut-claim a
value a caller can hold rather than a promise it must keep (xref:#witnessed-cut[below]); and
the `Scope` brand, which turns PRD 0013's created-order hazard from a documented discipline
into a compile error (xref:#restriction-scope[below]).
Orthogonal to the six primitives, the two lattice types also carry the *relative* reads
(xref:../../docs/prd/0013-metis-relative-base-change.adoc[PRD 0013], S89): `restrict`, base
change along a sub-roster inclusion, and `try_glue`, the *exact* descent fold beside the lax
`merge`, refusing an authority disagreement with a typed `Disagreement` witness. They are
reads on the `VersionVector` and `DotSet` families, not a primitive of their own; see
xref:#relative-reads[the relative reads] below. Beside them sit the *difference reads*
(xref:../../docs/prd/0014-metis-difference-reads.adoc[PRD 0014], S95), the anti-entropy
question "what do I owe you": `VersionVector::difference` is the owed set (the
co-Heyting residual, carrying claims to be reached, never subtracted counters) and
`DotSet::difference` enumerates the exact owed dots; each is documented in its type's
section below.
toc::[]
== Responsibility
`metis` is the decision layer: it _consumes_ stamps to reason about causality, the
capability a `Kairos` scalar alone cannot provide. A `Kairos` total order respects
causality but cannot _detect_ concurrency (two causally unrelated stamps still
compare). `metis` owns the structures that recover that distinction and act on it.
Two reasons to change this module: a new causal-reasoning primitive, or a change to
how an existing one decides ordered versus concurrent (the `VersionVector`), gates
delivery (the `Ideal`), mints and learns events (the `Producer`), computes
cross-node stability (the `Stability` tracker), records exact receipt (the
`DotSet` have-set), or merges causal state (the `Dotted` pair over the open
`DotStore` axis).
The module is pure `no_std`; the files that allocate import `alloc` explicitly
(`version_vector/mod.rs:1`, `version_vector/wire.rs:1`, `ideal/mod.rs:1`,
`stability/mod.rs:1`, the allocating `dot_set/` modules, and the `causal_store/`
modules), so it is
compiled on every target, default and `--no-default-features` alike, and needs no
feature gate. It depends on `kairos` for the `Kairos` stamp and the `station_id`
identity space it shares; it consumes no `chronos` source (causal reasoning is over
counts and stamps, not wall time).
== Type inventory
[cols="1,2,3",options="header"]
|===
| Type | Kind | Role
| `VersionVector` | struct over `BTreeMap<u32, u64>` | Per-station counts of observed
events; the (distributive) lattice that decides causal-ordered versus concurrent
(`version_vector/mod.rs:44`; lattice reads in `version_vector/lattice.rs:5`).
| `Iter<'a>` | borrowing iterator | Walks a vector's `(station_id, counter)` entries
in station order; the read side the buffer's gate uses (`version_vector/iter.rs:13`).
| `Gate` | trait (`Dep`, `Progress`, `deliverable`/`advance`/`stale`) | The buffer's stability
rule, the seam `Ideal` runs over (`gate/mod.rs:54`). Monotone; the machine passes the `sender`, so a
bare `Dep` need not name "self".
| `ReleaseDrivenGate` | marker capability over `Gate` | Every legal progress transition comes
from an admitted release. Required for `And`; intentionally absent from externally opened
`EpochGate`.
| `Causal` / `Fifo` | unit `Gate` impls | The two shipped leaf gates: causal happens-before
(`Dep = VersionVector`, `gate/causal.rs:13`) and the scalar per-source FIFO watermark
(`Dep = u64`, `gate/fifo.rs:20`). Peers; neither is a default.
| `And<A, B>` / `AndProgress<A, B>` | product `Gate` / nominal product progress |
Conjunctive composition (S237) over `ReleaseDrivenGate` components: both gates must deliver;
either may declare stale. The
progress type implements the componentwise information order rather than tuple
lexicographic order.
| `check_gate_laws` / `GateLawCheckError` | dependency-free conformance case checker / typed
failure | Checks one caller-generated ascending progress pair for the observable gate laws;
rejects descending and incomparable fixtures separately. Generator strategy and the dynamic
released-only proof remain caller-side.
| `Event<T, D>` | struct `(Kairos, D, T)` | A stamped event plus the gate's dependency *data* `D`
(causal: a `VersionVector`, the default); the unit the buffer orders (`event.rs:20`).
| `Ideal<T, G: Gate>` | struct over `G::Progress` + `Vec<Event<T, G::Dep>>` | The delivery machine
over a gate: accepts events out of order, releases them in `Kairos`-minimal order
(`ideal/mod.rs:57`); exposes the ready frontier read-only (`frontier`, `ideal/mod.rs:189`).
Aliases `CausalIdeal<T>` / `FifoIdeal<T>` name the gate.
| `AtCapacity<T, D>` | struct `(Event<T, D>, NonZeroUsize)` | The rejected outcome of the bounded
`Ideal::try_insert` (`ideal/capacity.rs:81`): the live backlog stayed full after reclamation, so
the event is handed back for the caller's give-up policy (delivery behavior is unchanged).
| `Producer<C = DynClock>` | struct over a sealed `ClockCarrier` + `VersionVector` | The send-side
BSS step: mints causal `Event`s through `now` and `observe`s received ones into knowledge and the
clock's receive rule, with `try_observe` the bounded receipt (`producer.rs:225`). `C` abstracts
clock *ownership* only (erased owned default, or inferred concrete owned,
`Arc<Clock<TS>>` / `&Clock<TS>` to share the station's one
clock, S73); the type stays causal-specific (R7) and the payload rides on `produce`/`observe`.
| `Stability` | struct over `BTreeMap<u32, VersionVector>` | The cross-node causal-stability
tracker (S78): a fixed, caller-declared roster, `report` join-folding each member's delivered
cut, `watermark` the n-ary meet, the greatest cut every member has passed
(`stability/mod.rs:75`, S142).
| `UnknownStation` | struct `(station: u32)` | The rejected outcome of `Stability::report`
(shared by `Purview::note` and `Retirement::acknowledge`): the reporter is not on the roster, so
the report was refused and the tracker is unchanged; admitting it would be a membership change,
the caller's policy (`stability/unknown.rs:10`, S142).
| `Abandoned`, `AbandonRefusal` | struct `(station, bound)`; enum | Departure (S336): the witness
`Stability::abandon` hands back, carrying the abandonment bound as the loss the decision writes
off, and the two refusals that keep the family a family (a non-member, and the last survivor)
(`stability/abandonment.rs`, ruling R-84).
| `DotSet` | struct over `BTreeMap<u32, StationDots>` | The exact have-set (S83): per station,
exactly which 1-based dots have been received, however disordered the arrival, compactly (a
gap-free floor plus the exceptions parked above it); exposes the bracketing cuts `floor` /
`high_water`, the `holes` fetch list, the union join `merge`, and a canonical run-length wire
frame (`to_bytes`, PRD 0016) (`dot_set/mod.rs:71`; compact station form in
`dot_set/station.rs:11`).
| `Disagreement` | struct `(station: u32, left: u64, right: u64)` | The rejected outcome of
`VersionVector::try_glue` (`version_vector/relative.rs:109`, S89): two partial views disagree on a
station both claim authority over, so no glued section exists and nothing was folded. Evidence,
not a verdict; which side over-claims is the caller's call (PRD 0013).
| `DotStore` | trait (`dots`/`is_bottom`/`causal_merge`/`causal_merge_from`/`restrict`/`support`/`novel_to`/`novel_to_witnessed`) | The open store
axis of the causal pair (S96): typed content addressed by dots, with the five trait laws
(support exactness, the survivor law, content-follows-the-dot, semilattice on covered pairs,
fiber-wise restriction) as contract (`causal_store/store.rs:51`). `DotSet` is the bare instance,
`DotFun<V>` the in-tree payload instance (S102); other payload stores are caller impls.
`causal_merge_from` (S182, ruling R-14) is the provided in-place form, default-bodied as the
pure merge, agreement the one added law; overriding is a cost seam, never semantics. The same
posture carries the two S191 (ruling R-21) provided reads: `support` (`causal_store/store.rs:136`,
the survivor coordinate as a have-set, defaulting to the `dots()` fold) and `novel_to_witnessed`
(`causal_store/store.rs:207`, the anti-entropy selection under a peer's recording-possession
claim, defaulting to the bare `novel_to`).
| `DotMap<K, S>` | struct over `BTreeMap<K, S>` | Caller-keyed composition of dot stores
(S144, `causal_store/dot_map/mod.rs:31`): per key a nested store, canonical (no bottom entries, so a key vanishes
with its last surviving dot), the *pair's* context vouching for every level. `K` is opaque, the
`Event<T>` payload posture. `insert` and the one-pass `from_disjoint` (`causal_store/dot_map/mod.rs:86`,
`causal_store/dot_map/mod.rs:120`) keep dots disjoint across keys (trait law 1);
`DotMapIter` (`causal_store/dot_map/iter.rs:8`) is its
borrowing iterator.
| `Dotted<S: DotStore>` | struct `(store: S, context: DotSet)` | The causal pair (S96,
`causal_store/pair/mod.rs:60`): what survives, bracketed by everything ever seen. `merge`
(`causal_store/pair/mod.rs:153`) is the only write (survivor law and knowledge join); `next_dot`
(`causal_store/pair/mod.rs:218`) assigns off the never-forgetting context; the anti-entropy reads
`delta_for` / `delta_for_witnessed` / `delta_for_since` ship the owed delta; state and delta are
one type.
| `UncoveredDot` | struct `(station: u32, dot: u64)` | The rejected outcome of `Dotted::try_new`
(`causal_store/pair/mod.rs:131`): the store carries a dot the context disowns, so the parts lie about
their past and no pair was built; the witness names the first such dot (`causal_store/pair/uncovered.rs:10`).
| `DotFun<V>` | struct over `BTreeMap<(u32, u64), V>` | The one value-carrying `DotStore` minerva
ships (S102/S145, `dot_fun/mod.rs:45`): per dot the value that write carried, the multi-value register
shape. Same-dot value discipline is *keep-self, equal by basis* (an honest dot names one write,
so two copies are equal; a disagreement is a basis violation out of scope). `values` reads the
surviving siblings; `observed` (`dot_fun/mod.rs:129`) is the register supersede-set.
| `DotFunIter<'a, V>` | borrowing iterator | Walks a `DotFun`'s `((station, dot), &value)` entries
ascending by dot (`dot_fun/iter.rs:7`).
| `DotCollision` | struct `(station: u32, dot: u64)` | The rejected outcome of
`DotMap::from_disjoint` (`causal_store/dot_map/collision.rs:11`): two keys' stores share a dot, so the batch has
no honest map (trait law 1); names the first colliding dot.
| `Composer<S>` | struct `(station: u32, state: Dotted<S>)` | The write-side facade over a causal
pair (S103/S112/S139, `composer/mod.rs:46`), the `Producer` analogue: `compose` runs the whole write
flow in one call (assign a fresh dot, cover the delta, merge locally, return the dot as receipt),
making the doomed-dot and uncovered-delta traps unbuildable; `absorb` is the receive half,
minting a `Received`. Mechanism, no policy. Run writes ride `compose` unchanged (S211, ruling
R-33: dots are per-station counters and the composer is its station's one writer, so a whole
`weave_run` reservation from the receipt dot is fresh by the context invariant; the rustdoc
carries the note).
| `Purview` | struct over `BTreeMap<u32, DotSet>` | The per-peer causal-context tracker (S105,
`purview/mod.rs:91`): per roster peer, a lower bound on the context that peer has seen, raised only
by `note`d `Received` evidence. The gossip-targeting dual of `Stability` (`owed` serves what a
peer provably lacks), one carrier down (contexts, not vectors).
| `Received` | struct `(from: u32, context: DotSet)` | Proof a context was received from a named
peer (S112, `purview/received.rs:22`): the only unaudited constructor is `Composer::absorb`, so
`Purview::note` reads peer and context out of the witness and the over-claim / misattribution
hazards are unrepresentable. `trust` (`purview/received.rs:61`) is the one audited escape.
| `Retirement` | struct over `BTreeMap<u32, DotSet>` | The cross-node *retirement* tracker (S115,
`retirement/mod.rs:60`, S141), the removal dual of `Stability`: the meet of every roster member's
acknowledged applied removals, the one claim `Rhapsody::condense` accepts. Application evidence,
not mint evidence, is its input.
| `Retired` | struct `(DotSet)` | Evidence a removal set has been applied at *every* roster member
(S115/S141, `retirement/retired.rs:41`): the private inner set leaves only `Retirement::retired` (the honest
meet) and the audited `trust` as constructors, so a bare `DotSet` cannot reach `condense`.
| `Cut` | struct `(VersionVector)` | A `VersionVector` witnessed *gap-free by construction* (S108/S140,
`attest/mod.rs:134`): the constructor set is closed over honest sources (`floor_of`, `delivered_by`,
`common_of`, `bottom`, and the meet/merge/restrict closure theorems), with no vector-taking
door, so holding one *is* evidence of honest local construction. Closes the PRD 0011 R8
cut-claim trap.
| `Scope<'brand>` / `Scoped<'brand, T>` | brand structs | The restriction scope (S109,
`scope/mod.rs:32`, `scope/scoped/mod.rs:52`, S143): `with_scope` mints a fresh invariant lifetime, and `Scoped` evidence
carries it, so comparing restrictions from two different scopes does not typecheck, making
PRD 0013's created-order hazard a compile error. `forget` is the named escape.
| `ScopedPeek<'a, T>` | display-only borrow | The hardened return of `Scoped::peek` (S114,
`scope/peek.rs:17`): `Debug` and `PartialEq` only, no `PartialOrd` / `Deref` / accessor, so no
scoped order verdict leaks out through a display read.
| `Node<K, V>` | struct over four component stores | The sparse-product node (S190, PRD 0020,
`node/mod.rs:100`): the kind closure of the axis, a kind-tag register (`DotFun<Kind>`) beside
register (`DotFun<V>`), map (`DotMap<K, Node>`, the recursion), and sequence (`Rhapsody`)
components under one identity, `DotStore` componentwise (`node/store.rs:23`). Writes refuse
cross-component straddles; `observed` (`node/mod.rs:247`) is the exclusive-write supersede-set;
re-kinding is one covered delta through `Composer::compose_super`.
| `Kind` | enum (`Register` / `Map` / `Sequence`) | A store *shape* a node carries content under,
never a meaning (`node/kind.rs:12`); the tag register's value type, ordered in the fixed
enumeration order.
| `Kinds` | `Copy` struct (three flags) | The evidenced-kind set (`node/kind.rs:31`), the value of
`Node::kinds_present` (`node/reads.rs:46`): tag claims plus shapes with surviving support;
empty means no surviving support of any kind.
| `KindPlurality` | struct `(kinds: Kinds)` | The refused outcome of `Node::sole`
(`node/kind.rs:120`): two or more kinds in evidence, so no single kind's content is honestly
projectable; carries the whole surfaced set for the caller's resolution.
| `NodeContent<'a, K, V>` | borrowing enum | One kind's content as `Node::sole` hands it out
(`node/reads.rs:13`): the typed projection that cannot read one kind's content for a node whose
evidence says another; a bottom component is the honest content of an empty node of its kind.
| `DecodeError` | `#[non_exhaustive]` enum | Typed failure of the `VersionVector` wire
decoder: unknown version, unexpected length, or non-canonical form (zero counter,
non-ascending stations) (`version_vector/wire.rs:169`).
| `HaveSetDecodeError` | `#[non_exhaustive]` enum | Typed failure of the `DotSet` have-set wire
decoder (PRD 0016): unknown version, unexpected length, or a non-canonical run frame (empty
station, non-ascending stations, zero-length or non-maximal run, run overflow, or a run past
the input-length dot budget) (`dot_set/wire/error.rs:11`). A separate codec from the vector's,
so a separate error (the PRD 0007 / `kairos` separation, one type down).
|===
`PartialOrd` is implemented on `VersionVector` (`version_vector/lattice.rs:126`); `Ord` deliberately is
not. Concurrent vectors are genuinely incomparable, so a total order would
misrepresent them. This is the type-level contrast with `Kairos`, whose derived `Ord`
_is_ total, and the contrast the buffer exploits: it uses the vector's partial order
to gate delivery and the stamp's total order to linearize the concurrent frontier.
== The lattice (`VersionVector`)
A version vector maps each `station_id` to a `u64` count of that station's events
this vector has observed. The structure is a bounded-below *distributive lattice*
(a join-semilattice until S78 carved the meet):
[horizontal]
bottom:: the empty vector (`new`, `version_vector/mod.rs:52`): every station at `0`.
order:: `a <= b` iff `a.get(s) <= b.get(s)` for every station `s`. This pointwise
order _is_ happens-before. Decided by `partial_cmp` (`version_vector/lattice.rs:126`).
join:: `merge` (`version_vector/lattice.rs:12`) is the pointwise maximum: the least upper bound, a node
that has seen everything either vector saw. Commutative, associative, idempotent.
meet:: `meet` (`version_vector/lattice.rs:45`, S78) is the pointwise minimum: the greatest lower
bound, what two vectors agree on. Dual to `merge`; absorption and both distributive laws are
pinned by the S78 property tests. Its n-ary form over a declared roster is the stability
watermark (xref:#stability-tracker[below]).
residual:: `difference` (`version_vector/lattice.rs:97`, S95) is the co-Heyting residual, the
third connective of the anti-entropy triad: the least vector whose `merge` into the
other side covers this one ("what do I owe you"). Specified by the Galois connection
`a.difference(&b) <= x` iff `a <= b.merge(&x)`, whose laws the adjoint ledger wrote
before the code existed (bottom iff dominated; repaying reaches exactly the join;
currying over creditors). The shape trap, pinned by example test: where the debtor
leads, the result carries the debtor's own count (the claim), never the subtraction,
because the owed events are the spans `(b(s), a(s)]` and a subtracted counter names
the wrong dots (PRD 0014).
step:: `increment` (`version_vector/mod.rs:77`) advances one station's counter by one (the only move
strictly up the order, _below the ceiling_: it saturates at `u64::MAX` rather than wrapping,
so at the ceiling it is a no-op and successive events would share a dot); `observe`
(`version_vector/mod.rs:89`) raises one station toward a count learned elsewhere.
read:: `iter` (`version_vector/mod.rs:104`) walks the `(station_id, counter)` entries in station
order, and `&VersionVector` is `IntoIterator`. Canonical form means every yielded
counter is `>= 1`. This is the read side the buffer's gate walks; exposing it keeps
the buffer off the private map.
The per-station counter is a lifetime-monotonic `u64`. It is deliberately *not*
`Kairos::logical`, the 16-bit Lamport tiebreak that resets when physical time
advances. The two are complementary: the stamp gives the total order to sort and
ship; the vector answers the causal questions the total order cannot. They share only
the `station_id` space.
[#canonical-form]
== Canonical form (the load-bearing invariant)
A station at count `0` is held *absent* from the map. So "absent equals zero," and
two vectors that mean the same thing compare equal and hash equally no matter how they
were built. The whole point: derived `Eq`/`Hash` are well-defined only because no
operation ever stores a zero.
Every mutator preserves this:
* `increment` writes `get(s).saturating_add(1)`, always `>= 1` (`version_vector/mod.rs:78`).
* `observe` inserts only when `counter > get(s)`, so the stored value is `> 0`;
`observe(s, 0)` is a no-op (`version_vector/mod.rs:89`).
* `merge` takes a max with `other`'s counters, which are themselves `> 0` (the other
vector is canonical), so no zero is introduced (`version_vector/lattice.rs:12`).
* `meet` keeps an entry only where the pointwise minimum is positive, so a station
absent from (or zero on) either side stays absent (`version_vector/lattice.rs:45`).
A change that lets a `0` reach the map silently breaks equality and hashing; that is
the first thing to check when touching a mutator. The buffer only _reads_ vectors
(`get`, `iter`, `merge`), so it cannot violate canonical form.
== Deciding the relation: `partial_cmp` walk-through
`partial_cmp` (`version_vector/lattice.rs:126`) returns `Some(Less | Greater)` for a strict
happens-before, `Some(Equal)` for identical vectors, and `None` for concurrent. It
tracks two flags over the union of stations:
. Walk `self`'s entries; for each, compare against `other.get(station)`. A station
where `self` is larger sets `self_leads`; smaller sets `other_leads`.
. A station present in `other` but absent from `self` reads as `0` here against a
positive count there (both canonical), so it sets `other_leads`. This is the
`keys().any(...)` check (`version_vector/lattice.rs:143`), which is why canonical form matters for the
decision, not just for equality.
. The flag pair decides: neither leads is `Equal`, exactly one leads is the strict
relation, both lead is concurrent (`None`).
Consistency with `Eq`: `partial_cmp` returns `Some(Equal)` exactly when no station
leads either way, i.e. when the maps are identical, i.e. when `self == other`. So the
partial order agrees with derived equality, as the `PartialOrd`/`PartialEq` contract
requires.
[#relative-reads]
== The relative reads: base change and descent (PRD 0013)
Every `metis` object is a family over the discrete station base: a dot _is_
`(station, dot)`, and canonical form _is_ finite support over the stations, so the dot
space is fibered over them. What the crate lacked was that reading's fundamental arrow,
base change. Two `VersionVector` methods carry it (with a `DotSet` twin,
xref:#have-set[below]), and because the base is a bare set of ids no topology or category
machinery enters the code
(xref:../../docs/prd/0013-metis-relative-base-change.adoc[PRD 0013] R1, S89).
[horizontal]
restrict:: `restrict(roster)` (`version_vector/relative.rs:36`) is base change along a
sub-roster inclusion: the vector's counts on the stations `roster` names, bottom
everywhere else. Functorial (identity on the full support, idempotent, composing by
roster intersection) and *exact* against every shipped fold and read (merge, meet, floor,
high water, holes, cut embedding). Restriction selects whole per-station fibers and never
enters one, so it commutes with the operations that also do not. The contrast is the
point: the merge/floor law is lax only because union crosses a fiber's interior, and
restriction never crosses one.
glue:: `try_glue(other, overlap)` (`version_vector/relative.rs:79`) is the *exact* descent fold
beside the lax join. `merge` resolves every disagreement by pointwise maximum, the right
fold for *knowledge* (the larger count is the newer fact) and the wrong one for
*authority*: where two partial views each claim a station and their counts differ, the max
fabricates a section nobody vouched for, over-claiming in the unrecoverable direction of a
cut (PRD 0011 R8). `try_glue` refuses instead, returning `Disagreement`
(`version_vector/relative.rs:109`) with the station and both counts. `overlap`, the stations
both sections speak for, is caller-declared in the `Stability`-roster mold: under
absent-equals-zero a vector carries no domain of its own, so which stations it vouches for
is a deployment fact. Sections cut from one vector always re-glue to it (the sheaf
condition in code); an empty overlap makes the check vacuous and the glue degenerates to
`merge`, deliberately.
*The witness travels one way* (PRD 0013 R3). Restriction _preserves_ order and _reflects_
concurrency, and neither converse holds: two concurrent vectors can restrict to ordered or
equal ones, because restriction can drop exactly the stations that witnessed the
disagreement. So a concurrency verdict on restrictions is global evidence, but an order
verdict certifies nothing beyond the sub-roster: restricted order is order _over the
sub-roster_, never order tout court. Comparing restrictions and acting as if the verdict
were global is the *created-order hazard*, the one PRD 0013 exists to name
(`test_restriction_creates_order` pins it). `try_glue` and `merge` both stay; no fold ever
resolves disagreeing authority by silent maximum (R5).
The asymmetry these reads exhibit (restriction sitting between its two Kan extensions; the
S83 floor / high-water pair as the two adjoint preservation theorems) is read as
adjunctions in xref:../../docs/metis-adjoint-ledger.adoc[the adjoint ledger], which sharpens
the pushforward refusal to its strongest form: two canonical pushforwards exist, so choosing
between them is policy and the machine never chooses.
[#wire-encoding]
== Wire encoding (PRD 0007)
`VersionVector` has a canonical, versioned byte frame, and the `Event` envelope
`(stamp, deps)` is composition over it. Specified in
xref:../../docs/prd/0007-metis-event-wire-encoding.adoc[PRD 0007], implemented in S16b; it
is the `metis` analogue of the `Kairos` codec (PRD 0002) and the variable-length half a
replication transport needs. The first concrete caller is `plethos`/`pinax`, shipping a
knowledge-vector digest across a process boundary.
[horizontal]
encode:: `to_bytes` (`version_vector/wire.rs:41`) writes `[version=0x01][u32 count][(station_id: u32,
counter: u64) x count]`, big-endian, entries in the map's ascending station order with
every counter `>= 1`. Infallible; the only allocation is the frame.
decode:: `from_prefix` (`version_vector/wire.rs:99`) is the parser; `from_bytes` (`version_vector/wire.rs:64`) is
`from_prefix` plus "the tail must be empty". `from_prefix` returns the vector and the
unconsumed tail, which is the envelope's payload.
Three properties make this more than a memcpy:
. *Canonical bijection, not a sort key.* Decode validates canonical form (`ZeroCounter`,
`NonAscendingStations`), not just structure, so it never fabricates a value the type's
own constructors cannot produce; encode is therefore a bijection between values and
valid frames, and byte-equality is value-equality. Unlike the `Kairos` frame (PRD 0002),
the bytes do *not* sort causally: a `VersionVector` is only partially ordered, so there
is no total byte order to preserve. The frame is a content hash or dedup key, not a
sorted-storage key.
. *Bounded allocation on untrusted input.* The required frame length is checked against
`bytes.len()` before the map is built, computed in `u64` so `count * 12` cannot overflow
`usize` on 32-bit `wasm32`. A tiny frame claiming a huge count is rejected in `O(1)`; the
fixed-width entry is what makes the bound structural. This is the crate's first
variable-length, untrusted-input parser, so it also has the crate's first `cargo-fuzz`
target (`fuzz/fuzz_targets/vv_from_bytes.rs`); since the parser became load-bearing at a
network boundary (`pinax`'s anti-entropy session, its S57), a second target,
`fuzz/fuzz_targets/envelope_from_prefix.rs`, drives the prefix seam under an adversarial
tail (S85, ruling R-8). The assurance above the fuzz targets divides by tool fit (S86,
ruling R-9 as amended): Kani proves the *heap-free fragment* (the length-check arithmetic
totally, sub-header rejection for all inputs; `version_vector/proofs.rs`), and the
map-touching laws are owned by *shaped* property tests (mutations of valid frames and
non-canonical two-entry frames, `tests/wire/vector/properties.rs`), because symbolic
`BTreeMap` structure is out of a bit-blasting solver's affordable scope. Creusot is the
chartered deductive rung for the rest, though the S94 probe
(xref:../../docs/horizons.adoc[horizons] Axis 5) found a deductive prover treats the sink
`insert` opaquely, so only the accept-path bijection needs its map model, while totality
and canonical rejection are map-free; it is deferred on the shipped-parser rewrite cost.
. *The envelope is composition, not a new frame.* An `Event` envelope `(stamp, deps)` is
the byte concatenation of the fixed 17-byte `Kairos` frame (PRD 0002) and the vector
frame; a decoder takes the first `kairos::KAIROS_WIRE_LEN` bytes as the stamp and
`from_prefix`-decodes the rest, leaving the payload tail. `metis` adds no `Event` codec
method, so payload framing stays the caller's concern.
`metis` owns its `DecodeError` (`version_vector/wire.rs:169`) rather than reuse `kairos::DecodeError`,
because canonical form is a `metis` concept; it may later *wrap* the `kairos` error for an
envelope codec, never the reverse (the dependency runs `metis -> kairos`).
== The delivery buffer (`Ideal`)
The buffer is the bridge PRD 0004 deferred and PRD 0005 specifies: the place the
total `Kairos` order and the partial happens-before order finally interlock. It maintains
the *order ideal* (down-set) of delivered events, accepting `Event`s (`event.rs:20`) in any
order and releasing their payloads so no event is delivered before the events it depends
on.
The delivered set is a *down-set*, not a directed ideal: this is the lattice sense of
"ideal". By Birkhoff representation the down-set and the delivered vector `D` are the same
object in two coordinates (events are the join-irreducibles; `D` counts, per station, how
many of its events lie in the set), which is why the buffer stores only `D` and leaves the
down-set implicit (xref:../../docs/cut-lattice-and-frontier.adoc[the cut-lattice note]).
An `Event<T>` is `(stamp: Kairos, deps: VersionVector, payload: T)`. The stamp's
`station_id()` is the sender; `deps` is the sender's observed-knowledge at send time
_including this event_, so `deps[sender]` is the event's own causal sequence number
(`>= 1`) and `deps[k]` for other `k` are its cross-station dependencies. This is the
Birman-Schiper-Stephenson causal-broadcast contract over the crate's own vector. The
buffer never inspects `payload`, so `T` is unbounded.
[#gate-seam]
=== The gate seam (PRD 0009)
`Ideal<T, G: Gate>` runs a fixed *machine* over a caller-chosen *gate* `G` (S27b). The machine
(holdback, `Kairos`-minimal release, forgetful `pop`) and its linearization are gate-independent;
the gate is the one rule that decides *when* an event is stable. The trait (`gate/mod.rs:54`) is three
stateless methods over an associated `Dep` (the per-event descriptor, `Event::deps`) and `Progress`
(the monotone state, bottom = `Default`):
[horizontal]
`deliverable(progress, sender, dep)`:: is the event releasable now.
`advance(progress, sender, dep)`:: fold a released event in, moving `progress` only *up*
(monotone; the load-bearing law). What it folds is the gate's choice (`Causal` the `dep` vector,
`Fifo` the sender's seq, the test `Quorum` the sender alone); for the shipped `VersionVector`
progresses it is the lattice join, but the machine needs only the rise (the
production-recording-decision note, finding 6).
`stale(progress, sender, dep)`:: can this event never become deliverable (drop it at `insert`).
The `sender` (`stamp.station_id()`) is a *machine* argument, not part of `Dep`: a bare descriptor
need not name "self", and folding identity into `Dep` would shadow the stamp and risk desync. The
gate never sees the stamp or the linearization (R2).
*`stale` is terminal, and load-bearing for two machine operations.* `stale` MUST be *terminal*:
up-closed in progress (once stale, stale for good) and disjoint from `deliverable`. That is what
lets `insert` drop a stale event and the bounded `try_insert` reclaim a pending one
(xref:#bounded-insert[`prune_stale`], below) on the strength of the current progress alone. The
joint up-set of `deliverable || stale` is a *third independent law*, not a consequence of those
two (amended S337; `check_gate_laws` has always checked it separately, and a gate with
`deliverable(p) = (p == 0)` and `stale` always false satisfies both of the above while stranding
its events). For the shipped gates it holds because the causal contiguity `deps[s] == D[s] + 1` is
an *equality*, true at one point and false again once `D[s]` overshoots, so `deliverable` alone is
not up-closed and terminal `stale` carves the overshoot out of the effective domain. Any `Gate`
whose `deliverable` is an equality must pair it with such a `stale`; a revisable / retrodictive
gate whose `stale` is not terminal must report `stale == false` instead, which discharges the
third law only where its `deliverable` is independently up-closed
(xref:../../docs/metis-gate-stale-contract.adoc[the gate-stale-contract note], R1).
Two leaf gates ship, as *peers* (neither a default): `Causal` (`gate/causal.rs:10`, below) and the
scalar `Fifo` (`gate/fifo.rs:16`), `Dep = u64` and `Progress` a `VersionVector` watermark map, per-source FIFO
with *no* cross-source clause (a strict deletion of `Causal`'s completeness, so it cannot regress
the default, and a `Dep` that is not a `VersionVector`). A non-causal *participation* / quorum gate
is a caller's, consumed as a fold; a test-only `Quorum` proves the seam carries the threshold shape
without shipping it.
S237 adds the caller-fired product `And<A, B>`. Its dependency is
`(A::Dep, B::Dep)`; release requires both component gates, advances both, and is terminally stale
when either component is stale. Both components implement `ReleaseDrivenGate`, asserting that
release is their only progress authority; `EpochGate` is excluded because adoption is a separate
checked transition. `AndProgress<A::Progress, B::Progress>` is nominal because Rust
tuples compare lexicographically, not in the componentwise product order the gate laws require.
Crossed progress states are therefore incomparable by type rather than a caller convention.
==== The causal gate (`Causal`)
The buffer holds a *delivered vector* `D` (`delivered`, the `Causal`-only reader at
`ideal/mod.rs:84`):
the per-sender count of events it has released, starting at bottom. An event `e` from sender `s` is
_deliverable_ against `D` (`Causal::deliverable`, `gate/causal.rs:19`) iff:
[horizontal]
contiguity:: `e.deps.get(s) == D.get(s) + 1`: the very next event from `s`, no gap and
no duplicate.
causal completeness:: `e.deps.get(k) <= D.get(k)` for every other station `k` the
event depends on (walked through `iter`): everything the sender had seen is already
released here.
Release advances `D := D.merge(&e.deps)` (`pop_ready` through `Causal::advance`, `gate/causal.rs:29`). Given
the two conditions the merge bumps only `s`'s entry by one, so the lattice join _is_ the
delivery step. Canonical form carries the edge cases for free: a dependency on a
never-heard station reads `D.get(k) == 0`, so the event waits; the first event from a
new sender is deliverable exactly when `e.deps.get(s) == 1`.
[#ready-antichain]
=== The frontier (the ready antichain)
Several pending events can be deliverable at once. Generically this set is the gate's
*enabled set*: the buffered events `deliverable` against the current progress, and it is an
*epistemic, local* frontier (the minimal deliverable events that _have arrived_, a subset of
the global `min(E \ I)`, never the whole of it). Under the `Causal` gate it has the
order-theoretic reading: the minimal undelivered events, pairwise concurrent in a
duplicate-free valid history, an *antichain* of the event order and the *cover* of the
delivered ideal; the scalar `Fifo` gate has the same reading per source. But the `Gate` trait
exposes no event order, so "antichain" is a `Causal` / `Fifo` property, not a guarantee of
every gate (a threshold gate enables events ordered by their thresholds, not an antichain);
see xref:../../docs/metis-production-recording-decision.adoc[the production-recording-decision
note]. Under `Causal` the delivered vector `D` is a *point* in the lattice of consistent cuts
(Mattern's lattice of global states, a run-dependent sublattice of the vector lattice), `merge`
the join it inherits, and the frontier the outgoing cover edges from that point. This is the
one place the gate falls silent and the next step is genuinely open, the τύχη the layer's
cunning is for.
The cover is the *leading* edge, and it lives outside the ideal: the minimal not-yet-delivered
events whose release would extend the down-set. It is not the ideal's *generating* antichain
`max(I)` (the maximal _delivered_ events, the trailing edge inside the ideal, which is the
ideal's Alexandrov boundary), and the buffer never materializes that set. Keeping the leading,
trailing, and spectral frontiers distinct is the subject of
xref:../../docs/cut-lattice-and-frontier.adoc[the cut-lattice note].
`pop_ready` linearizes that antichain by releasing its `Kairos`-minimal member first
(`next_deliverable`, `ideal/mod.rs:196`, a flat min-stamp scan). The linearization never
contradicts the happens-before order, because `a -> b` implies `a.stamp < b.stamp`: the
gate already enforces order, and the stamp only ranks events the gate leaves unordered. The
release order is therefore a function of the event multiset, not of arrival order, which is
what makes the buffer property-testable.
`pop_ready` returns the payload alone, the decided stream. The full-event `pop_ready_event`
(S32b, later strengthened at the release-provenance boundary) returns `Released<T, G>`, an affine
witness branded by the gate that completed the release. It contains the whole `Event`, `stamp` and
`deps` included, so a caller can tell which adjacent releases were causally forced and which were a
`Kairos` tiebreak between concurrent events: the linearization is a *decision* over the partial
order, and the payload stream alone cannot distinguish it from the causal order it derives from
(xref:../../docs/metis-production-recording-decision.adoc[the production-recording-decision
note]). `pop_ready` is its explicit payload projection, byte-for-byte the same stream.
This is the material a _deinotēs_ resolver (PRD 0008) or a retrodictive gate (PRD 0010) reads.
`frontier` (`ideal/mod.rs:189`) surfaces that same set read-only, a lazily filtered borrowing
iterator with the default linearization untouched, so a caller can resolve a genuinely
open frontier its own way (keep every sibling, pick a different winner, fold a join)
instead of taking the `Kairos`-minimal default. It is the caller-owned material the
_deinotēs_ dimension needs (PRD 0008): the buffer computes the antichain; what it becomes
is the caller's call. The set is a true antichain only in a valid history; the buffer
does not deduplicate, so a pre-delivery duplicate can appear beside its twin (a shared
dot, not a concurrency), which a resolver would collapse.
=== Totality and dropping
`insert` (`ideal/mod.rs:95`) and `pop_ready` never fail or panic, matching infallible stamp
generation and the version vector's total operations. `insert` drops an event whose
own dot is not ahead of `D[sender]` (`deps[sender] <= D[sender]`): a duplicate or stale
replay that can never become deliverable, including a malformed self-dot of `0`.
Out-of-order events wait.
[#bounded-insert]
=== Bounded insert (`try_insert`, S30)
`insert` buffers unconditionally, so an event whose dependencies never arrive grows `pending`
without bound (the lossy-channel reality below). `try_insert` (`ideal/capacity.rs:34`) is the additive
bounded path: it takes a `NonZeroUsize` `capacity`, and when the *live* backlog is already at
`capacity` it returns `AtCapacity` (`ideal/capacity.rs:81`) carrying the rejected event, leaving the
buffer unchanged. The infallible `insert` and the unbounded `new`/`Default` are untouched; the
bound is a property of the *call*, not a stored buffer field, mirroring the
`observe`/`try_observe` escape-hatch the error model describes. This is the materials split of the PRD 0005 pending-bound
non-goal: `metis` owns the *bound* (a mechanism), the caller owns the *give-up policy* (evict,
deadline, shed; any bound can drop a still-needed dependency, so that choice cannot be baked in).
When at capacity, `try_insert` first reclaims provably-dead entries through `prune_stale`
(`ideal/capacity.rs:59`): a `Vec::retain` dropping every pending event the gate now reports
`stale`, the lingering twin of buffer note 1. So the bound counts only events that can still be
delivered, and the `O(pending)` reclamation scan is paid only on the full path, never the common
one. `prune_stale` is behavior-preserving for delivery because `Gate::stale` is terminal (a
once-stale event stays dead, so it would never have been released; see
xref:../../docs/metis-gate-stale-contract.adoc[the gate-stale-contract note]), so causal safety,
exactly-once, and the frontier order are all unchanged.
[#bounded-causal-replacement]
=== Causal-safe replacement (`try_insert_evicting_where`, S236)
Replacement is available only on `Ideal<T, Causal>`. At capacity, Minerva excludes any
resident named in the causal past of the arrival or another pending event, then presents the
remaining candidates to caller policy in `Kairos` order. The first accepted candidate is
replaced atomically and returned through `BoundedInsert::Evicted`; no replacement advances
delivered progress.
This is the exact single-victim rule for valid causal histories: removing a causally maximal
resident creates no new missing predecessor among retained events. The `O(pending^2)` scan is
paid only on the contested full path. Priority, retry, quarantine, and shedding remain caller
policy. Eventual progress still depends on predecessor arrival and local release eligibility.
[#buffer-hazards]
=== Buffer notes for a future editor
. *A pre-delivery duplicate lingers, but is never released twice.* `insert` only drops
events already overtaken by `D`. Two copies inserted _before_ the first is delivered
both buffer; one is released, the twin then fails contiguity forever and sits in
`pending` until the buffer is dropped. Exactly-once still holds (the twin never
releases). `insert` never prunes such provably-dead entries (it is beyond the signed-off
PRD 0005 algorithm and would tax the common path), so `pending_len` is an _upper_ bound under
duplicate floods. The bounded `try_insert` (S30) _does_ reclaim them, but only on its full
path (see xref:#bounded-insert[bounded insert]); the unbounded `insert` path is unchanged.
. *No built-in pending bound; an opt-in one.* An event whose dependencies never arrive waits
forever, inherent to causal delivery over a lossy channel. `pending_len` (`ideal/mod.rs:145`) is
exposed for monitoring, and `insert` stays unbounded. The opt-in bound is `try_insert` (S30,
xref:#bounded-insert[above]): it caps the live backlog and hands a rejected event back. The
*give-up policy* (evict, timeout, shed) stays a deployment concern (PRD 0005 non-goal).
. *Order by stamp only.* `next_deliverable` keys on `Event::stamp`. Stamps are unique
across a valid history (per-station monotone, distinct `station_id` low bits), so the
minimum is unambiguous; do not key the frontier on the payload.
== The event producer (`Producer`)
The *send* half of causal broadcast, the inverse of the buffer's gate. A `Producer<C = DynClock>`
(`producer.rs:72`) holds one station's send-side context: a `Clock<TS>` (identity + stamp source +
high-water), reached through the sealed `ClockCarrier` capability `C`, and a `VersionVector` of
observed-knowledge. It is the per-station logic the S14b history generator ran inline, now a
shipped type.
[horizontal]
send:: `produce` (`producer.rs:161`) is the Birman-Schiper-Stephenson send step: increment
`knowledge[self]` (`self` is `clock.station_id()`), snapshot the result as the event's
`deps` (so `deps[self]` is the event's own dot, `>= 1`), mint a `Kairos` with `now`, and
return the `Event`. A plain `now` suffices because the clock is the high-water (below).
receive:: `observe` (`producer.rs:194`) is the dual: fold a received event's `deps` into
`knowledge` (`merge`) and advance the clock past the event's stamp with `Clock::observe`
(S20, the HLC receive rule). It is the only way a producer learns another station's
progress, and it is *receipt*, not application delivery: a node observes an arrival into its
causal context before the buffer's `pop_ready` delivers it (the Birman-Schiper-Stephenson
receive-versus-deliver split, xref:../../docs/metis-production-recording-decision.adoc[the
production-recording-decision note]).
bounded receive:: `try_observe` (`producer.rs:225`, S73) is `observe` behind the
`Clock::try_observe` skew bound (S41), all-or-nothing across the whole receipt: on `Ok` the
effect is exactly `observe`, on `Err(SkewExceeded)` *neither* knowledge nor clock changed.
The pairing is the point: minerva does not expose a knowledge-merge without the stamp fold,
because folding a rejected event's `deps` alone would let a later `produce` snapshot
dependencies its minted stamp does not dominate, breaking the embedding of causal order in
stamp order.
=== Clock ownership is a parameter (S73)
`Producer::new` once took its `Clock` by value only, which contradicted the station invariant
(one station, one logical clock) for any station with stamping sites beyond the producer: the
first such consumer (`ethos`, whose station clock also stamps seals and ledger appends through an
`Arc<Clock<TS>>`) could not construct a `Producer` at all without minting a second clock under the
same `station_id`. S73 generalized the carrier. S291 makes the source concrete and the
capability explicit: `Producer<C = DynClock>` accepts an owned `Clock<TS>`, an
`Arc<Clock<TS>>`, or a `&Clock<TS>` through sealed `ClockCarrier`. Semantics do not
depend on `C`; the lock-free clock already tolerated concurrent stamping. The one discipline the
type cannot enforce: share the clock across stamping *sites*, not the producer *role*. Two
producers over one clock would each self-count `knowledge[self]` and mint colliding dots.
=== The clock is the high-water (S21)
The producer once carried its own `Option<Kairos>` high-water (`latest`), folded into the
next mint through `after(latest)`. S20 added `Clock::observe`, the pure HLC receive rule, and
S21 retired the field: `observe` now calls `clock.observe(event.stamp)`, so the clock
itself tracks everything observed, and `produce` mints through `now` alone. One high-water,
held where time already lives, instead of a second copy shadowing the clock.
This is _behavior-changing_, not a transparent refactor. `Clock::observe` is a receive _event_:
it ticks logical time once per call, even for a stamp already dominated (it is not an
idempotent merge; S20). So routing receipts through it means each `observe` ticks the
clock, and a produced stamp can land a logical step (or more, under repeated equal-physical
receipts) above where the old `after(latest)` put it. Every ordering invariant is
preserved (monotonicity, causality `a -> b => a.stamp < b.stamp`, and dominance over every
observed stamp); only the free-running logical tiebreak, which carries no meaning, shifts.
=== Order-robust learning (compose, do not own)
Folding into `knowledge` uses `merge`, a join (commutative, associative, idempotent) over a
causally closed `deps`, so it is order-independent. The clock's receive rule is _not_ a join
(it ticks per call), so the clock's exact logical value depends on how many events are
observed; but the property a later `produce` needs, that its stamp dominates every
observed stamp, holds in any arrival order. That is what lets a `Producer` _compose_ with a
`Ideal` instead of owning one: a node feeds each arrival to its producer (to observe)
and inserts it into its buffer (to reorder for the application), and the buffer needs no
change. The two are orthogonal materials wired by the caller, not a bundled endpoint (a
unified `Station` is a deferred PRD 0006 non-goal).
Self-echo is _safe_ but no longer a literal no-op: observing a producer's own event back
cannot raise `knowledge[self]` (already at that dot), but it does tick the clock once like
any receipt. So only the *buffer* must never be fed a node's own events (it would mis-gate);
the producer tolerates the echo, paying one harmless logical tick.
[#producer-hazards]
=== Producer notes for a future editor
. *Not generic over the payload, on purpose.* `Producer` stores no payload, so it is not
`Producer<T>`; the payload rides on `produce`/`observe`. The lone asymmetry with `Event<T>` /
`Ideal<T>`, taken so the struct never encodes a type it does not hold. The `C` parameter
(S73) is not an exception: it abstracts how the clock the producer *does* hold is held,
never what it stamps.
. *Single-owner, `&mut self`.* No interior synchronization; a multi-threaded node owns one
per thread or wraps it. The lock-free `Clock` inside already tolerates sharing, which is
what makes the shared-carrier forms (`Arc<Clock<TS>>`, `&Clock<TS>`) sound.
. *Identity is single-sourced.* `station_id()` (`producer.rs:239`) reads `clock.station_id()`;
the producer never stores a second id that could disagree. S73 cost it `const`: the read goes
through the carrier capability, whose trait method is not const.
. *`observe` ticks the clock (S21).* It routes every receipt through `Clock::observe`, so it
is not idempotent on the clock; redundant or echoed receipts advance logical time.
Harmless (ordering invariants hold), but do not assume `observe` leaves the clock untouched.
. *`observe` is receipt, not delivery (S32c).* Renamed from `deliver`: in
Birman-Schiper-Stephenson "deliver" is the ordered application release, which is the buffer's
`pop_ready`; the producer's step is receipt. The knowledge it builds is therefore
observed-knowledge (generally ahead of what the buffer has delivered).
[#stability-tracker]
== The stability tracker (`Stability`)
The fourth primitive (S78): the cross-node *meet*, specified in
xref:../../docs/prd/0011-metis-causal-stability-watermark.adoc[PRD 0011] and built under owner
ruling R-6 (`owner-comments.adoc`) as the retention face of the crate's bounded-resources
boundary, beside the backlog bound (`try_insert`, S30) and the skew bound (`try_observe`, S41).
A `Stability` (`stability/mod.rs:75`, S78/S142) holds a fixed, caller-declared roster of `station_id`s, each
slot the join of every delivered cut that member has reported; construction (`new`,
`stability/mod.rs:113`) seeds every slot at bottom.
[horizontal]
report:: `report(station, &delivered)` (`stability/mod.rs:138`) join-folds a member's delivered cut
into its slot. The join makes reporting idempotent, commutative, and monotone, so duplicated,
reordered, or stale gossip is absorbed and the watermark never regresses. A non-roster
reporter is refused with `UnknownStation` (`stability/unknown.rs:10`), tracker unchanged: admitting
it would silently change what "stable" means, a membership decision that is the caller's.
watermark:: `watermark()` (`stability/mod.rs:199`) computes the n-ary meet across every slot: the
greatest cut every member has passed, hence delivered everywhere, hence safe to forget
(Mattern: consistent cuts are closed under pointwise min, so the watermark is itself a cut).
An unreported member holds bottom and pins the watermark there (nothing is stable until
everyone vouches), and the empty roster answers bottom rather than the vacuous top (the
mathematical meet of an empty family), because a safe-to-forget quantity must never be
fabricated. Computed on read, `O(roster x entries)`; no cache to keep coherent.
witnessed:: `report_cut(station, &Cut)` and `watermark_cut() -> Option<Cut>` (`stability/mod.rs:164`,
`:274`, S114) are the witnessed twins: `report_cut` carries a `Cut` to the boundary instead of
laundering it through `Cut::as_vector`, and `watermark_cut` hands the meet back branded when
every report so far arrived witnessed (`None` the moment one bare `report` lands, since a mixed
family's meet cannot be forged into a witness). The value equals `watermark()` always; only the
gap-freedom proof is conditional (xref:#witnessed-cut[the witnessed cut]).
read:: `reports()` (`stability/mod.rs:249`) walks the `(station, vouched cut)` slots in station
order, so the straggler pinning the watermark is observable.
depart:: `abandon(station) -> Result<Abandoned, AbandonRefusal>` (`stability/mod.rs:275`, S336)
is the one door that narrows the family the meet ranges over, and the crate's whole membership
mechanism. The roster is untouched, a departed member's dots stay lawful history that sealed
records name, and `Epochs` is untouched too. Irreversible, because un-abandoning would lower
a watermark; refused for a non-member and for the family's last survivor.
`abandonment_bound(station)` prices the decision in advance (the surviving members' join
restricted at that coordinate, PRD 0013), `Abandoned` returns it as the loss written off, and
`resurgent()` names abandoned members whose slot absorbed a report afterwards, the little
the tracker can observe about a premature eviction, and no verdict. Bare abandonment reaches the
watermark and stops there: the epoch rounds keep ranging over the whole roster, because
narrowing them on a *local* bound seals a record the consignment door then rejects, one door
after the lineage has advanced
(xref:../../docs/metis-membership-departure.adoc#where-departure-stops[the departure note]).
attest:: `Departure` (`stability/departure.rs:51`, S339) is the round that closes it. `opened(station,
survivors)` opens it over the family that remains; `propose(held, successor)` contributes this
replica's gap-free prefix of the departing station's dots *and fences there in the same act*
(`Ragged` for a holding above its own floor, `SuccessorHeld` for one already folded into the
plane the open epoch founds, `FenceBroken` for a second proposal that exceeds the first, `Impersonated` for a report carrying the station whose slot this round owns, which is
what makes a sealed round imply that *this* replica fenced); `reinstate(prefix)` is the replay
door a restart re-enters through, at the value it durably recorded rather than one re-derived; `fold` absorbs peers' proposals by max under `Vouched`; `try_seal` mints the
`Departed` at their join and raises the fence to it. `admits(dot)` is the fence
verdict for the old plane and `admits_successor` for the plane the epoch founds, where the
coordinate is bottom from the moment the round opens (both take a `Dot`, so the old
counter-zero "not a dot" arm is unrepresentable, ruling R-91); `Fenced::is_resurgence` is true exactly
when the round had sealed, the crate's only
resurgence evidence, as against `resurgent`'s prompt. `abandon_attested(&Departed)` narrows
exactly as `abandon` does, checks that the attestation's family covers its own
(`FamilyMismatch`) and that some remaining member can still serve the bound
(`StrandsAttestation`, which both doors carry: a bound is a promise somebody holds what is
below it), and records the agreed bound, which `attested(station)` reads and the
epoch rounds substitute for the departed member's testimony, unconditionally. `refounded` on
both types carries a departure across a seal at the evictee's compacted prefix in the
consigned base, derived inside the door from the base it is handed, bottom exactly when
nothing of the evictee's survived, since a bound is a counter in a plane the re-foundation
re-mints, and the base prefix is that plane's own coordinate for the member (amended at S343,
ruling R-90; xref:../../docs/prd/0026-metis-membership-departure-round.adoc[PRD 0026] R8).
=== Stability notes for a future editor
. *Report delivered cuts, not observed knowledge.* The meaningful input is an
application-delivery cut (`Ideal::delivered` / `progress`), never a `Producer`'s
receipt-level `knowledge`, which runs ahead: feeding it would declare stability for events a
peer has received but not applied. This is the sharpest instance of the counter-meaning
hazard below (vectors carrying different meanings do not mix).
. *The roster is fixed on purpose, and only departure moves the family.* Dynamic membership
re-defines the watermark (a joiner must regress it, a leaver un-pins it) and interacts with
state already reclaimed below the old watermark; both are policy. Arrival still means "build a
new tracker over the new roster"; departure does not, because a lineage cannot cross a roster
change (`EpochLedgerRehydrateError::RosterMismatch`) and a substitute report is refused at the
confirmation door, and both are pinned. `abandon` is that one narrowing, and it is
caller-declared configuration
rather than machine state: a rebuilt tracker starts whole again and the departure must be
re-declared (`tests/membership.rs`). `abandon_attested` adds the agreed bound the epoch rounds
read and nothing else: the family narrows identically either way.
. *The tracker forgets nothing and has no wire form.* It computes the greatest safe cut;
reclamation below it is the caller's act in the caller's store, and reports travel as
PRD 0007 `VersionVector` frames or however the caller gossips.
[#have-set]
== The exact have-set (`DotSet`)
The fifth primitive (S83): the receipt-side record, specified in
xref:../../docs/prd/0012-metis-dot-set-exact-have-set.adoc[PRD 0012] and built under owner
ruling R-7 (`owner-comments.adoc`) as the constructive discharge of PRD 0011 R8 (a stability
report is a gap-free *cut claim* the tracker cannot verify). A `DotSet` (`dot_set/mod.rs:71`)
holds, per station, exactly which 1-based dots have been received, however disordered the
arrival, in the standard compact form (`StationDots`, `dot_set/station.rs:11`): the gap-free prefix
`1..=floor` plus a sparse exceptions set parked above it, re-absorbed the moment a hole
fills, so in-order receipt costs what a bare counter costs and equality is
path-independent (canonical form, the vector's doctrine one type up).
[horizontal]
record:: `insert(station, dot)` (`dot_set/mod.rs`) records a receipt, idempotently and in
any order; the non-dot `0` is refused (`observe(s, 0)`'s mirror). `contains`
(`dot_set/mod.rs`) is the exact membership read; `merge` (`dot_set/algebra.rs`) is the
union, the join of the have-set lattice; `from_witnessed` embeds a witnessed cut (the public
door; the bare-vector `from_cut` is `pub(crate)`, for the in-crate closure theorems only).
bracket:: `floor()` (`dot_set/mod.rs`) is the greatest gap-free prefix, the have-set's
lattice *interior*: a genuine cut by construction, the honest `Stability` report, monotone
and never over-claiming. `high_water()` (`dot_set/mod.rs`) is the per-station maximum, the
cover of the down-closure: the liveness quantity (a `pinax` `Horizon` in `metis` basis)
that must never be reported as stability. The floor is only *lax* under `merge` while the
high water is a join homomorphism; the strict case (two sides filling each other's holes)
is why exchanging have-sets beats exchanging floors (the cut-lattice note's have-set
section).
repair:: `holes()` (`dot_set/reads.rs`) lazily names every missing dot below the high water,
the whole-set fetch list, with `holes_for(station)` its per-station
view and `hole_count()` the repair-debt norm computed in
`O(stations + exceptions)` without enumerating a gap (both S98, PRD 0016);
`exceptions_len()` counts the dots parked out of order, the
observability read for the type's one unbounded axis (bounding it is the caller's policy,
the S30 logic). `station_count`, `station`, and `stations` expose the compact nonempty rows as
typed `DotSetStation` summaries without materializing either bracketing vector; each summary
fixes station, floor, high water, and forward gap in one allocation-free read.
wire:: `to_bytes` / `from_bytes` / `from_prefix` (`dot_set/wire/mod.rs:79`, `:110`, `:155`, S98,
PRD 0016) are the canonical run-length frame, the deferred S84 half now shipped: each
station's exceptions compressed as maximal runs of consecutive dots, decode validating
canonical form and rejecting every shape no encoder emits (`HaveSetDecodeError`,
`dot_set/wire/error.rs:11`). It is the `DotSet` analogue of the `VersionVector` frame
(xref:#wire-encoding[above]) with one added trust obligation the run form carries: a run is a
*decompression* (a 16-byte run names arbitrarily many dots), so decode charges every run
against a *dot budget* (`RunTooLong`) and refuses a frame that would materialize more
dots than the budget justifies. Standalone the budget is the input byte length; an
embedding codec whose validated structure or resource policy bounds the honest set passes
`HaveSetDecodeBudget` through `from_bytes_with_budget` or
`from_prefix_with_budget` (`dot_set/wire/mod.rs`, public since S242; S197 first supplied
the internal seam):
both rhapsody frames pass their decoded skeleton's cardinality, which keeps a legal
dense-above-a-hole visible suffix decodable and prefix acceptance tail-independent,
the S197 gate review's finding; Polis S3 passes its validated exception ceiling, the
first out-of-tree shape). A v1 byte-identity contract like the vector
frame; a v2 is a sibling codec, never an in-place change, and transport stays the caller's.
owed:: `difference(other)` (`dot_set/reads.rs`, S95) lazily enumerates every dot held here
and lacked there, ascending, the serve list dual to `holes()`'s fetch list; in fact both
shipped asymmetries are its special cases (the holes are the closure's difference
against the set, the exceptions the set's difference against its interior, pinned by
property test), and between genuine cuts it enumerates exactly the spans
`VersionVector::difference` names (PRD 0014). Unlike `holes()` it cannot be inflated
by an adversarially high dot: it yields only held dots.
relative:: `restrict(roster)` (`dot_set/algebra.rs:27`, S89) is the have-set base change, the
`VersionVector::restrict` twin (xref:#relative-reads[above]): the same dots on the roster's
stations, nothing elsewhere. Selecting whole fibers, it commutes *exactly* with every read
and fold (`merge`, `floor`, `high_water`, `holes`, `from_cut`), the exactness the vector's
floor-under-`merge` law gives up (PRD 0013).
=== Have-set notes for a future editor
. *The basis is 1-based dots, and only the basis is fixed.* A dot is "the `k`-th event
from the station," `k >= 1` (`deps.get(sender)` for producer-minted events); a 0-based
consumer maps `dot = sequence + 1` at its own boundary. What a dot *means* (received,
applied, persisted) is the caller's; a `Stability` report needs an application-delivery
have-set's floor (the counter-meaning hazard below).
. *The wire frame and repair reads shipped; the capacity bound and coupling did not.* The
run-length frame and the per-station repair reads (`holes_for`, `hole_count`) landed as
xref:../../docs/prd/0016-metis-have-set-wire-frame.adoc[PRD 0016] (S98, the `wire` and
`repair` entries above); adoption stays consumer-gated. Still deferred and caller-side: the
bounded-exceptions `try_insert` variant (the S30 sequence, waiting on a capacity caller), the
`Stability` coupling (the tracker keeps accepting plain vectors), and every transport
decision. They grow on first consumer contact (PRD 0012 R7).
. *Keep the absorb invariant.* Every mutation path must leave `above` strictly above
`floor + 1` (`absorb`, `dot_set/station.rs:65`); a parked dot at `floor + 1` would break
path-independent equality, the exact-set property tests catch it.
[#causal-store]
== The causal store algebra (`Dotted`, PRD 0015)
The sixth primitive (S96, ruling R-12): replicated state that can *remove*. A
`Dotted<S>` (`causal_store/pair/mod.rs:60`) pairs a store of dot-tagged content with the causal
context of every dot ever seen; the context never forgets, so absence splits exactly
("in the context, not the store" is seen-and-dropped; "not in the context" is
never-seen), and the merge honors removals without tombstones.
[horizontal]
axis:: `DotStore` (`causal_store/store.rs:51`) is the open store seam, the `Gate` posture:
five laws in the trait contract (support exactness; the survivor law; content follows
the dot; semilattice on covered pairs; fiber-wise restriction), three in-tree instances
(`DotSet` as bare presence, `causal_store/store.rs:140`; `DotMap<K, S>` composition,
`causal_store/dot_map/store.rs:10`; the value-carrying `DotFun<V>`, xref:#payload-store[below]),
other payload stores caller-side. `DotMap::insert` and the one-pass `from_disjoint`
(`causal_store/dot_map/mod.rs:86`, `causal_store/dot_map/mod.rs:120`, refusing `DotCollision`,
`causal_store/dot_map/collision.rs:11`) enforce law 1's
cross-key dot disjointness.
merge:: `Dotted::merge` (`causal_store/pair/mod.rs:153`) is the pair's *only* write: the store
coordinate folds by the survivor law (a dot survives iff both stores hold it, or one
holds it and the other's context never saw it; for `DotSet` stores that is
`intersect` plus the two `difference`-against-context legs, `causal_store/store.rs:150`),
the context coordinate by the knowledge join. Deliberately *not* the product join:
the store's shortfall below the plain union is exactly the superseded dots (the
adjoint ledger's causal-pair section). The same write ships in place since S182
(ruling R-14): `Dotted::merge_from` (`causal_store/pair/mod.rs:181`) delegates to the
axis's provided `causal_merge_from` (default-bodied as the pure merge, the `clone_from`
precedent) and grows the context by exactly the delta's stations, observationally
identical and delta-bounded where the overrides land (`DotSet`'s residual-edit fold,
`causal_store/store.rs:163`, over the crate-internal store-role `remove`;
`Rhapsody`'s incremental skeleton-and-index insertion). The S181 scale probe measured
the pure form linear in the document per composed keystroke; the agreement law is
pinned per store, per pair, and in the foreign conformance harness.
assign:: `Dotted::next_dot` (`causal_store/pair/mod.rs:218`) reads one past the *context's* high
water (`DotSet::high_water_of`). Assignment must consult the
structure that never forgets: a store-based assignment re-issues a superseded dot and
every peer that saw it drops the new write silently (the *doomed dot*). There is no
eager-reserving variant on purpose: an in-session design cut had one, and the first
simulated write exposed it discarding its own delta (the dot pre-reserved in the live
context read as seen-and-dropped at merge time). The merge records the dot; nothing
else does. PRD 0015's write-path-trap section is the standing record.
delta:: The pair is state *and* delta in one type, so anti-entropy is a read.
`DotStore::novel_to(context)` (`causal_store/store.rs:172`, S97) is the store fragment a peer
holding `context` has not seen, content preserved. `Dotted::delta_for(peer_context)`
(`causal_store/pair/delta.rs:58`, S97) builds the minimal owed delta against a peer's *exact*
context: the novel store, plus a context carrying every *removal* whole (never trimmed,
or a drop the peer also saw is lost) but *only* removals (a shared survivor's coverage
would spuriously supersede it), the pair's own asymmetry applied to the delta.
`Dotted::delta_for_witnessed(peer_context, peer_recording)`
(`causal_store/pair/delta.rs:87`, S191, ruling R-21) is the same framing under a
*recording-possession witness*: a store carrying a recording plane beside its support (the
sequence store's skeleton) withholds exactly what the peer claims to hold, possession claimed
directly licensing the sub-selection a survivor context cannot (the S190 law), and the witness
is a claim whose failure directions are safe (under-claim over-serves; over-claim starves only
the claimant). The arc-10 instrument is the license: the bare read measured O(document) per
probe on both axes (17.1 ms and a 2,752,542-byte fragment for one owed keystroke at 65k chars,
16.6 ms for a peer owed nothing), the witnessed read ~440 ns and 84 bytes, flat across sizes.
`Dotted::delta_for_since(&Cut)` (`causal_store/pair/delta.rs:177`, S113) is the whole-state twin
against a witnessed peer *floor*: it carries the whole survivor store and folds the
contiguous prefix into one floor (reclaiming the context frame, not the store transfer),
and the parameter is a `Cut`, never a bare vector, because the seed asserts gap-freedom
below it (xref:#witnessed-cut[below]).
boundary:: `Dotted::try_new` (`causal_store/pair/mod.rs:131`) is where foreign pairs enter:
coveredness (every store dot in the context) is a construction fact on every shipped
path and a typed refusal (`UncoveredDot`, first witness in ascending order) at the
boundary, because an uncovered pair lies about its own past and the survivor law
would double-deliver it.
[#payload-store]
=== The payload store (`DotFun`)
`DotFun<V>` (`dot_fun/mod.rs:45`, S102/S145) is the one value-carrying `DotStore` minerva ships:
per dot the value that write carried, the multi-value register shape from the delta-CRDT
literature (dots to values). A bare register is a `Dotted<DotFun<V>>` (concurrent writes
are sibling dots, both readable through `values`, `dot_fun/mod.rs:114`); a keyed register map is a
`Dotted<DotMap<K, DotFun<V>>>`. It closes the axis's one missing shape: the intro's "payload
stores are the caller's" now names a single in-tree exception.
The whole discipline is *keep-self, equal by basis*, and it is why the store needs no
`V: Eq` bound. Trait law 3 (content follows the dot) says a surviving dot keeps the content
its store attached, and the merge never invents or reassigns it. On the honest basis a dot
names exactly one write, so a dot carried by two stores was minted once and carries one
value: the copies are equal, and `causal_merge` keeps self's. A same-dot *disagreement* (one
dot, two different values) is a basis violation of the class the clock already trusts away, a
reused `station_id`, and this store deliberately does not police it: an `Eq`-plus-fallback
path would hide the corruption and a panic path would turn a peer's Byzantine act into a
local crash, both worse than stating the basis plainly. `insert` (`dot_fun/mod.rs:88`) refuses a
duplicate dot (content is never reassigned) and the non-dot `0`; `observed` (`dot_fun/mod.rs:129`)
is the register supersede-set (exactly the store's live dots as a `DotSet`), the argument a
register-style write hands `Composer::compose_super`.
=== Causal-store notes for a future editor
. *The recipes are tests, not types.* Add-wins sets, observed removes, register-style
supersession: each is a delta-construction discipline exercised in
`tests/causal_store/` and documented in the consumer guide; shipping one as a type
would own its application semantics (R-12's boundary). Keep it that way. The lone
shipped store beyond the dot-shaped pair is `DotFun<V>` (S102, above), value-carrying
but still semantics-free: it holds the caller's `V` without reading it.
. *Contexts are the pair's, never per-component.* One context vouches for every
nesting level of a composed store; threading per-key contexts would break
coveredness checking and the composition's free laws.
. *A caller `DotStore` impl owes law 3 its own test.* The axis is value-opaque (`dots`
yields identities, never content), so a generic conformance harness cannot reach
content-follows-the-dot; `tests/causal_store/foreign/` shows the shape to copy, an
out-of-tree register store checked against its own accessors beside the shipped
instances. Stokes `0a14aae` is the first external implementation: an inverse-indexed
effect store whose generated partition schedules compare its in-place merge with the
canonical `DotMap` result. Its representation invariant remains in its own suite, as
this boundary requires.
[#composer]
== The write-side facade (`Composer`)
`Composer<S>` (`composer/mod.rs:46`, S103/S139; the compose *receipt* is S112; the flows fold
in place through `Dotted::merge_from` since S182, behavior-identical and delta-bounded, ruling
R-14) is to the causal
pair what the `Producer` is to events: the write-side facade that makes the send discipline
*structural* rather than remembered. A `Dotted<S>` is the kernel, and its write flow has two
sequencing obligations a hand-roller can forget, both failing in the unrecoverable
direction:
* *Merge before the next dot.* `next_dot` reads the never-forgetting context, so a delta
must be merged locally before the next dot is assigned, or the same dot is re-issued and
every peer whose context already covers it drops the second write (the *doomed dot*).
* *Cover the store.* A write that supersedes builds its delta through `try_new`, whose
context must contain every store dot, or the build is refused (`UncoveredDot`).
`Composer` closes both from inside. It holds the pair as `state` and updates it on every
local write, so the next assignment reads a context that already carries the last dot,
making freshness a fact of the flow rather than a rule the caller keeps.
[horizontal]
compose:: `compose(weave)` (`composer/mod.rs:150`) runs the whole flow in one call: assign the
fresh dot, hand it to `weave` (which returns the delta's store and the dots it supersedes),
assemble the delta context as (superseded) union (the store's own dots) so it is *covered
by construction*, merge locally, and return `(dot, delta)`. The returned dot is the
*receipt* (S112): a caller keying an out-of-band payload channel reads the dot from the
receipt, never by re-deriving it through `next_dot` before the call, which a merge landing in
between would make a doomed dot. Coverage holds by construction, so the `try_new` refusal
arm is an unreachable documented fallback (a store under-reporting its support rides the
lie through, the honest degraded outcome for a store the crate cannot see into, pinned by
`test_compose_over_a_lying_store_rides_the_lie_through`).
compose_super:: `compose_super(weave, superseded)` (`composer/mod.rs:178`) is the register write,
taking the supersede-set as a *closure over the held store* computed at the write, closing
the read-then-compose TOCTOU a pre-read supersede-set opens (`DotFun::observed` is the
canonical argument).
retract:: `retract(superseded)` (`composer/mod.rs:220`) is the observed-remove flow: a
pure-context delta (`Dotted::from_context`) superseding exactly those dots, merged and
returned. Which dots ride is the caller's semantics (add-wins versus remove-wins);
`Composer` does not choose.
absorb:: `absorb(from, delta)` (`composer/mod.rs:241`) is the receive half: merge a peer's delta
or full state (they are one type) and return a `Received` receipt pairing `from` with the
delta's own context. It is the only unaudited way to mint a `Received`, which is what makes
`Purview::note` safe by construction (xref:#purview[below]).
owed:: `owed_to(peer_context)` (`composer/mod.rs:254`) delegates to `Dotted::delta_for`, the
minimal delta that converges a peer whose context is known; `owed_to_witnessed`
(`composer/mod.rs:270`, S191) is the witnessed sibling a steady-state anti-entropy loop
should run.
resume:: `adopt(station, state)` (`composer/mod.rs:72`) resumes over persisted state (the
caller's durability; persist-then-send is the caller's discipline, PRD 0015); `condense`
(`composer/condense.rs:28`, `Composer<Rhapsody>` only) is GC through the facade
(xref:#sequence-store[below]).
`Composer` owns *mechanism and no policy*: no transport, no persistence, no add-wins /
remove-wins choice. It is the `Producer` posture one axis over.
[#purview]
== The gossip tracker (`Purview`, `Received`)
`Purview` (`purview/mod.rs:91`, S105) is the per-peer causal-context tracker, the
*gossip-targeting* dual of `Stability`. Where `Stability` folds each roster member's
*delivered cut* and reads their meet (the retention watermark, "what may I forget"),
`Purview` folds each member's *seen context* and reads the per-peer residual ("what do you
provably lack"): the same roster-fixed, bottom-defaulting tracker shape, one carrier down (a
`DotSet` context here, a `VersionVector` cut there).
[horizontal]
row:: each roster peer has a row from birth, at bottom, raised only by `note`
(`purview/mod.rs:155`) folding `Received` evidence by union. The row is a *lower bound* on what
the peer has seen, and that direction is the whole safety story: an under-claimed row makes
`owed` re-ship dots the peer already holds (a harmless liveness cost the merge absorbs),
while an over-claimed row omits dots the peer lacks and stalls convergence *silently*, the
unsafe direction no mechanism here can detect.
owed:: `owed(state, peer)` (`purview/mod.rs:188`) is `Dotted::delta_for` against the row: what
`state` holds that the peer provably lacks. Because the row is a lower bound, it over-ships,
never under-ships.
common:: `common()` (`purview/mod.rs:206`) is the n-ary `intersect` of the rows, the dots every
peer provably holds (meet-shaped, so an unreported peer pins it at bottom and an empty
roster answers bottom, never the vacuous top); `common_floor()` (`purview/mod.rs:224`) is its
gap-free floor, the honest bridge to a `Stability`-shaped read (and the source of
`Cut::common_of`, xref:#witnessed-cut[below]).
The type's one hazard is made *constructional*. An over-claim stalls convergence silently,
so `note` takes a `Received`, not a bare `(u32, &DotSet)`. A `Received` (`purview/received.rs:22`,
S112) records two facts a receive path can *prove*, the peer and the context that peer
demonstrably held (a peer cannot ship what it has not seen), and its only unaudited
constructor is `Composer::absorb`. So the two hazards `note` once left to prose,
over-claiming a context the peer never had and misattributing it to the wrong peer, are both
unrepresentable: peer and context are read *out of* the witness (a `compile_fail` doctest
pins that a bare `DotSet` no longer notes). The one deliberate door out is `Received::trust`
(`purview/received.rs:61`), for a full-state exchange the receive path cannot witness; the name is the
warning, and only a `trust` over-claim can still stall convergence.
[#retirement]
== The retirement tracker (`Retirement`, `Retired`)
`Retirement` (`retirement/mod.rs:60`, S115/S141) is the cross-node tracker of *applied removals*, the
removal dual of `Stability`: where `Stability` tracks how far each member has *received*,
this tracks which removed dots each member has *applied*. It exists for one caller,
`Rhapsody::condense` (xref:#sequence-store[below]), which may excise an order tombstone only
once its dot is removed and applied at every replica that will ever write again;
over-claiming strands a laggard's future anchor forever, the unrecoverable direction.
[horizontal]
input:: `acknowledge(station, applied)` (`retirement/mod.rs:97`) join-folds a roster member's
acknowledged applied-removal set, off-roster stations refused (`UnknownStation`). *Mint
evidence is the wrong witness*: removal deltas mint no dot, so "everyone applied this
deletion" is not derivable from a `Cut` or the `Stability` watermark (those witness what
was *seen*, not *applied*). The input is application evidence only the deployment can
gather (an ack round, an epoch, a quorum sweep), the same standing-claims posture as
PRD 0011 R8.
claim:: `retired()` (`retirement/mod.rs:121`) is the n-ary `intersect` of the members'
applied-sets, the dots *every* member has acknowledged (monotone; an unreported member pins
it at bottom; the empty roster answers bottom, never the vacuous "everything is retired").
It returns a `Retired`, not a bare `DotSet`.
`Retired` (`retirement/retired.rs:41`, S115/S141) is the one claim `condense` accepts. Its inner `DotSet`
is private, so the only constructors are `Retirement::retired` (the honest meet) and the
audited `Retired::trust` (`retirement/retired.rs:77`); a bare `DotSet` no longer condenses (a
`compile_fail` doctest pins it), so the over-claim that stranded a laggard's anchor is
unconstructible. `trust` is the escape for a caller who gathered application evidence some
other way (the studio's global-oracle scan stands in for the deployment's ack round); the
name is the warning, and the burden is total and unrecoverable.
[#witnessed-cut]
== The witnessed cut (`Cut`)
`Cut` (`attest/mod.rs:134`, S108/S140) is a `VersionVector` witnessed *gap-free by construction*: a
genuine cut, not an upper bound running past holes. It closes the PRD 0011 R8 trap that a
`Stability` report is a *cut claim* the tracker cannot verify, and that the honest cut and
the over-claiming high-water are the *same type*, a bare `VersionVector`, indistinguishable
at every boundary. PRD 0012's `floor` made an honest cut *constructible*; `Cut` carries the
proof in the type.
The mechanism is a *closed constructor set*. There is deliberately no `From<VersionVector>`,
no `new(vector)`, no `Default`, no `Deref`, no public field, and no `serde` or wire path (a
vector decoded from the network is a *claim* and stays one; `Cut` witnesses *local*
construction only, exactly the R8 division). Every constructor is a read off a
gap-free-by-construction source or a closure theorem over cuts already witnessed: `bottom`
(`attest/sources.rs:11`), `floor_of` (`attest/sources.rs:22`, PRD 0012's interior),
`delivered_by` (`attest/sources.rs:35`, gate contiguity), `common_of`
(`attest/sources.rs:47`, a `Purview` floor), and the `meet` / `merge` / `restrict`
closures (`attest/lattice.rs:14` on), each a *theorem* about the
vector lattice (the min, max, or fiber-selection of gap-free prefixes is gap-free) and each
pinned by a property test. This is the discipline PRD 0012's Alternatives section demanded
when it rejected a `Horizon`-style marker newtype: an assertion moves the trap to its
constructor; a construction removes it. Four `compile_fail` doctests pin the absent doors
(`Cut(v)`, `Cut::from(v)`, `Cut::default()`, `&Cut` deref).
The bridge out is one-way. `as_vector` (`attest/views.rs:13`) borrows and `into_vector`
(`attest/views.rs:24`) surrenders the witnessed vector; a bare vector cannot come back, because no
vector-taking constructor exists (`from_witnessed`, `attest/sources.rs:63`, is `pub(crate)` and
gated). That one-way surrender is what makes `Cut` a zero-friction adoption:
`Stability::report_cut(peer, &cut)` and `Stability::watermark_cut() -> Option<Cut>` (S114)
carry the witness through the tracker without laundering it through `as_vector`, the meet of
a witnessed family being a cut by the closure theorems (the `Option` is `None` the moment one
bare charter `report` lands, since a mixed family's meet cannot be forged into a witness), and
`Dotted::delta_for_since(&Cut)` (above) takes the witness because its floored seed asserts
gap-freedom. `difference` (`attest/lattice.rs:75`) returns a bare `VersionVector`, not a `Cut`, on
purpose: the co-Heyting residual is a per-station *claim* ("raise to here"), the top of an
owed span, not a down-set prefix, so it is exact but not a cut. `Cut` is evidence about the
*moment of construction*: monotone sources keep it from ever becoming a lie, but a newer floor
can make it *stale*, and staleness is the caller's clock, not the type's.
[#restriction-scope]
== Restriction scopes (`Scope`, `Scoped`, `ScopedPeek`)
The `Scope` brand (S109) turns PRD 0013's *created-order hazard* from a documented discipline
into a compile error. Restriction preserves order but does not reflect it, so an order verdict
on restrictions is order *over the roster*, never order tout court; a caller comparing
restrictions from two different rosters and acting as if the verdict were global has
fabricated a happens-before out of forgetting.
`with_scope(roster, body)` (`scope/mod.rs:129`) mints a fresh, *invariant* lifetime `'brand` and
hands the body a `Scope<'brand>`. Restricting through it (`restrict`, `restrict_dots`,
`restrict_all`) yields `Scoped<'brand, T>` evidence (`scope/scoped/mod.rs:52`) carrying that brand, so
two values born under different scopes never unify: a cross-scope comparison does not
typecheck. The brand certifies the *invocation*, not the roster value, so even two
`with_scope([1], ..)` calls over identical rosters do not unify (they are two acts of
restriction). A `Scoped` value cannot escape `body` while branded (its type mentions
`'brand`); the lawful exit is `forget` (`scope/scoped/vector.rs:83` for vectors), the named escape that drops the brand
and the memory of the roster the verdict was valid over.
The polarity is the whole point (PRD 0013 R3, the one-way witness):
[horizontal]
order stays branded:: `partial_cmp_scoped` / `happens_before` (`scope/scoped/vector.rs:19`, `:29`) are
sound *within* the scope and inexpressible across it; `Scoped` deliberately has no
`PartialOrd`, so the `<` / `<=` operators cannot be reached and generic code bounded on
`PartialOrd` cannot compare scoped evidence as if the verdict were global.
concurrency escapes:: `concurrent_globally` (`scope/scoped/vector.rs:43`) returns a plain unbranded `bool`,
because concurrency *reflects* globally (the two leading stations survive in the roster); it
lawfully leaves the scope.
folds stay scoped:: `merge` / `meet` / `intersect` / `floor` / `map` keep the brand, since
restriction is a lattice homomorphism (folding restrictions equals restricting the fold);
`floor_cut` (`scope/scoped/dot_set.rs:69`) mints a branded `Cut` from the have-set floor without dropping
the scope.
`ScopedPeek` (`scope/peek.rs:17`, S114) is the hardened return of `Scoped::peek`: a display-only
borrow with `Debug` and `PartialEq` but no `PartialOrd`, no `Deref`, and no accessor handing
the inner reference back, so a scoped order verdict cannot walk out the display door (a bare
`&VersionVector` would reopen exactly the hole the brand closes). Two peeks compare equal but
never ordered; that asymmetry is the whole point.
[#sequence-store]
== The sequence store (`Rhapsody`)
The sequence instance of the `DotStore` axis, `Rhapsody` (S101, PRD 0017), is a large
self-contained subsystem, so it earns its own co-located note rather than a section here:
xref:rhapsody/mod.adoc[`src/metis/rhapsody/mod.adoc`]. In brief, an element's identity is a
dot, its place a `Locus` (the sided `Anchor` it hangs on, a dot with a before/after side or
the origin, and the `Kairos` rank ordering it among its siblings), deletion is causal
invisibility, and the ordering skeleton persists as order tombstones so a deleted element's
followers stay in place; `order()` reads a document order out of the two coordinates by an
iterative (never recursive) in-order skeleton walk over a maintained child index, and
`condense` (gated on a `Retired` witness, above) excises order tombstones once retired
everywhere. Its wire frame, anchoring rule, and full test map are in that note.
== The node store (`Node`, PRD 0020)
The kind closure of the axis (S190, ruling R-20): the recursive sparse product. Four
components under one identity, each a shipped store: `tag: DotFun<Kind>` (the kind
register; `Kind` is a shape, `Register` / `Map` / `Sequence`, never a meaning),
`register: DotFun<V>`, `children: DotMap<K, Node<K, V>>` (the recursion; a heterogeneous
tree is one pair), and `sequence: Rhapsody`. The `DotStore` instance is componentwise in
every method, so the axis laws are inherited component by component (the store-algebra
note owns the closure argument; `prop_node_conforms_to_the_axis` runs it). Implementation
notes a future editor needs:
* *The boxed enumeration leg.* `Node::dots` chains the four components, and the map leg
is type-erased (`Box<dyn Iterator>`) because the node recurses through `DotMap<K,
Node>`: an unboxed chain makes the opaque return type a member of its own definition
(rustc's E0275 cycle). A type-level necessity, not a cost choice.
* *Support exactness is a write discipline.* Every write method (`write_tag`,
`write_register`, `insert_child`, `weave`) refuses a dot another component carries,
reading causal support (`dots()`; a sequence order-tombstone is not support). Held
state is written only by merge, so the scans price delta construction, not folds.
* *Kind evidence rides surviving support.* `kinds_present()` is tag claims plus shapes
with surviving dots; a sequence reduced to tombstones evidences nothing (the
production-recording-decision separation applied inside the store), so `sole()`'s
`Ok(None)` means "no surviving support", which on a residue-only node is not bottom.
* *The exclusive re-kind is a recipe over `observed()`.* One `compose_super` whose store
is the fresh tag write and whose supersede read is `Node::observed` makes the
reassignment one covered delta; the atomicity is property-pinned, and the machinery is
all `Composer`'s (nothing node-specific was added to the facade).
* *No wire frame.* Deltas ship under the pair's context frame; a node codec would make
merge and read depth adversarial, so it enters, if ever, as a sibling codec with a
depth budget and worklist folds (PRD 0020 R7). Depth today is caller-built, exhibited
at 64 levels in the depth test.
== The mark store (`Scholia`, PRD 0021)
The annotation instance of the axis (S195, ruling R-23): dot-tagged spans over a
sequence's identity space. A `Scholion<T>` is one mark (`start` / `end`, each a `Verge`,
plus a caller-opaque `tag`); `Scholia<T>` is the store, structurally the payload store
applied to spans (`DotFun<Scholion<T>>` with pure delegation for its `DotStore` instance,
so every axis law is inherited and the conformance harness holds it beside the other
instances, `prop_scholia_conforms_to_the_axis`). The `Verge` vocabulary and the
projection read (`Rhapsody::extent`, whose verdicts are total: covered with emptiness
honest, inverted surfaced, dangling surfaced per end) live with the sequence store,
because comparing span boundaries through order-tombstone slots is the one read the
public walk cannot express (the rhapsody note's extent rows carry the shape and cost).
Sharing and editing are the register recipes verbatim (mint with `compose`, edit as a
whole-scholion `compose_super` over the mark's dot, remove with `retract`; concurrent
edits are surfaced siblings); `anchor_dots()` is the retention interlock's read (the
pin set a condense cadence subtracts, policy caller-side); expansion at a span's edges
is the side choice at mint, never a stored behavior field; and what a tag means never
enters the crate (the mechanics-versus-meaning boundary, R-23).
== The move record (`Metatheses`, PRD 0022)
The movement instance of the axis (S196, ruling R-24), stage C's reorder half. A
`Metathesis { target, to }` is one placement testimony, an existing element (`target`, a
dot whose identity never changes) re-placed at a new `Locus`; `Metatheses` is the store,
structurally the payload store applied to movement (`DotFun<Metathesis>` with pure
delegation for its `DotStore` instance, so every axis law is inherited and the conformance
harness holds it beside the other instances, `prop_metatheses_conforms_to_the_axis`). The
one load-bearing idea is that *a move is a second placement testimony for an existing
identity*, the same `(dot, Locus)` shape a weave records, so the record needs no new merge
semantics: concurrent moves of one element are surfaced sibling testimonies, resolved only
in the read. It lives in its own causal pair beside the text's (the parallel-pair recipe
the mark store also uses), so moving is `compose`, re-moving tidily is `compose_super`
over `moves_of(target)`, and undo is `retract` of the testimony's dot, convergent by the
survivor law like every other removal. The decision, which testimony wins and which is
refused, is the recension read (`Rhapsody::recension -> Recension`; since S203 also
maintained, `Recension::collate`, ruling R-30), documented with the
sequence store because it replays over the skeleton (the rhapsody note's recension rows
carry the replay rule, the sealed-view discipline, the collation, and the cost). The record never
chooses: the winner is the highest-rank surviving non-refused testimony by the fixed
public `Kairos` order, and every refusal (a cycle-former) is surfaced, detaching nothing.
== The epoch lifecycle (`Epochs`, PRD 0024 stage two)
The re-foundation rounds over the stability witness (S218, ruling R-37): one
replica's record of *when a re-foundation is licensed and settled*, and
nothing else. A `Declaration` ("re-found at cut `C`") is minted only through
`Epochs::declare`, whose license is `Stability::watermark_cut` and nothing
else (`EpochRefusal::Unwitnessed`; the carried `Cut` brand is the witness),
risen to the caller-declared epoch basis (`EpochRefusal::Unrisen` below it,
the R1 risen half since S222, ruling R-40: witnessed is not risen, a fresh
tracker witnesses the bottom cut; `deliver` refuses the same way, so a
vacuous peer declaration refuses identically everywhere instead of opening
a window no replica can adopt),
and carries a durable `EpochAddress` (seal-advanced lineage generation plus
its minting dot), so concurrent declarations and post-horizon tuple reuse are
distinct rather than confused epochs. Delivery is
provisional: members keep minting old-addressed, each confirms with its
delivered cut, and once the delivery watermark covers the join of every
member's confirmation cut the candidate set is provably complete and every
replica fixes the same winner by the fixed public `(rank, dot)` rule,
latched monotonically (`fixed`), losers surfaced as candidates until the
seal. `adopt` is the guard the charter's R5 states ("no replica mints
natively before the confirmation watermark fixes the winner"): it refuses
`Unconfirmed` until the round completes, then folds the member's own-station
adoption report. `try_seal` fires when the watermark covers the adoption
join: the window closes, and the sealed join retires into the lineage as the
R6 duplicate recognizer, retained for the caller-declared last-`k` horizon
(the S30 capacity idiom). `recognize` answers old-addressed traffic:
covered means duplicate (absorb), uncovered is the typed `AddressMiss`, an
open window routes to the shadow, and below the horizon the
machine refuses to guess (`BeyondHorizon`). Minting causally after a
delivered declaration and before the seal is `WindowOpen`, and an unknown
candidate arriving after the round completed locally is the same refusal
(the completed round proves it cannot lawfully exist). Mechanism, not
policy: cadence, transport, and the roster are the caller's, and the roster
must be the same family the caller's `Stability` tracker declares. The
fold the rounds license is `Rhapsody::refound` (stage one); the shadow,
projection, and epoch gate are the stage-three boundary below; the address
primitive moved into that boundary because the gate and recognizer require
it. Consumer payload translation remains stage four.
== The epoch boundary (`EpochShadow`, `EpochGate`, `EpochConsignment`, PRD 0024 stages three and four)
`Epochs::adopt` returns `Adopted`, the opaque proof that confirmation fixed
this winner locally. `EpochStratum::new` requires it and consumes text and
movement pairs containing no identity above the declaration cut; above-cut
state is window traffic, never fold input. Their contexts must also jointly
cover the cut, so partial below-cut snapshots cannot freeze a map.
`EpochShadow` owns that validated
state for one open window. Its `RefoundMap` binds the affine ceilings to the
adopted cut, not sparse woven high water; its `Recension` is the
maintained old-world judgment, and `EpochProjection` is the exact visible
identity sequence in the winner's plane, materialized lazily and cached until
the next delivery. `deliver_text` validates every woven locus, visible or not,
and rejects a
at-cut dot with no frozen image as `SweptIdentity` before mutation;
`deliver_moves` keeps the complete surviving testimony set, so an earlier
arrival may deterministically re-decide a retained move. The shadow is not
cloneable and exposes no seal claim. Its lifetime ends at the seal, through
the one witnessed door below.
Stage four's document-plane half (S263, ruling R-50) is
`EpochShadow::consign(self, &SealedEpoch)`: the shadow, consumed at the
seal it was opened for, derives the next generation's opening base pair
(`EpochConsignment`) as a pure function of its final delta set and the frozen
map, and returns beside it the `Consigned` witness (S335, ruling R-83) that
is the certifiable grade of the seal record itself. The spelling is `refound`'s own, applied to the final reading's
tombstone-inclusive slot order (streamed one leaf at a time): a window-born
survivor is woven at its judged place, a window-moved image sits where the
old replay put it, a window-deleted cut-live image keeps its locus as an
order tombstone for the native anchors that still name it, a
window-born-and-dead identity crosses as context only, and an identity dead
at the cut does not cross at all. The movement record is reborn empty
(carrying testimonies would re-judge them against the re-founded topology,
the S213 flip; the rank-contest falsifier records why verbatim anchors
cannot carry either), both pairs share one structurally translated context
(per-station live prefixes, affine window ranges, sparse exceptions) so each
plane's floors are born gap-free, and the retired map rides along as the
consumer half's translation seam (R7). The door checks everything the seal
witness implies: `ForeignSeal` refuses a mismatched epoch, `Incomplete`
refuses a sealed-join delivery the shadow never received, `BeyondSeal`
refuses carried post-seal traffic, `Unfoldable` refuses a reading a lawful
seal cannot contain, and every refusal hands the shadow back (boxed) so a
missing delivery is delivered and retried. The coverage record is the
seal's own: `Epochs` keeps a receipt-time protocol ledger of every
declaration dot received (verdict-independent, so displaced provisional
records and their forward-order refusals seal identically), canonicalized
against the adoption join at the seal, and `SealedEpoch::declaration_dots`
is its read.
The acceptance half of that door is a shipped type rather than a stated
duty. A `SealedEpoch` handed back by `Epochs::try_seal` proves only that
this replica's rounds completed; the consignment door is the first and only
place the record meets a *second, independent* source, because the sealed
join is assembled from peer reports while the coverage check reads the
deltas actually delivered. So the door is the sole mint of `Consigned`, a
caller binds a checkpoint certificate or digest over `Consigned::record`,
and the one audited escape `Consigned::vouch` has exactly two honest
callers, both restore doors (a bootstrapped joiner's verified peer claims,
and a rehydrated machine's own storage, whose checkpoint was written at a
seal and therefore past this door). Acceptance stays a *local* fact: it is
not a quorum, not a signature, and not evidence that a peer accepted the
same record.
One recipe duty rides the carry: native movement testimonies
wait for the seal, because a window move can flip a native verdict against
the re-spelled base (the deferral duty in the fleet's module note).
The representation is live for the window. The S210 fixture's compact
snapshot already reaches 13,239,562 bytes at one million events; decoding
that basis on every old-addressed arrival would abandon the pair's
delta-bounded merge and `Recension::collate` paths. A condensed idle mode
would need an arrival-cadence measurement before it could repay that cost.
Native events use `EpochIdeal<T>` (`Ideal<T, EpochGate>`). The dependency is
the winning declaration dot. Nothing releases before adoption;
`adopt_epoch` requires `Adopted`, folds that witness, releases only the winner, prunes
losing-address events as terminally stale, and refuses a later competing
adoption as `EpochAdoptionMismatch`. The generic mechanism addition is
the crate-private `Ideal::advance_progress` fold. Only the checked
`adopt_epoch` capability is public, so a causal buffer cannot skip releases
by forging external progress.
[#hazards]
== Hazards for a future editor (`VersionVector`)
. *Never let a zero counter into the map.* Canonical form is what makes `Eq`/`Hash` and
the concurrency decision correct. Every mutator is written to avoid it; a new one
must too.
. *Do not derive or implement `Ord`.* The order is genuinely partial. `Ord` would force
a total order onto concurrent vectors, the exact error the type exists to prevent. Use
`PartialOrd` and the `happens_before` / `concurrent` helpers.
. *`!(a <= b)` is not `a > b` here.* For a partial order the negation also covers the
concurrent case, so clippy's `neg_cmp_op_on_partial_ord` rejects it. Express intent
through `happens_before` / `concurrent` instead (the tests do).
. *The counter's _meaning_ is the consumer's, and two consumers do not mix.* The type is a
per-`station_id` `u64` count lattice; what a count _means_ is caller-defined. `metis`
itself already reads it two ways, the `Producer`'s observed-knowledge (receipt-level) and the
`Ideal`'s released-count `D` (application-delivery-level), and a consumer may add a third (for example a
replication sequence watermark). Vectors carrying different meanings over the same
`station_id` space are *not* interchangeable, though they compare and merge structurally.
A node running both a `Producer` and such a consumer holds two distinct vectors; do not
feed one where the other is expected (the consumer seam `plethos` ADR-0010 records).
+
The sharpest form of this mismatch is the *index basis*. `metis` is 1-based: an event's dot
is `deps.get(sender) >= 1` (the first event makes the count `1`), so the buffer's "next owed
from `s`" is the *strict* `dot > D.get(s)` (from contiguity `deps.get(s) == D.get(s) + 1`,
`is_deliverable` at `ideal/mod.rs:206`). A consumer keying on a 0-based `sequence` instead asks the
*non-strict* `sequence >= watermark.get(s)` (its watermark counts events seen, i.e. the next
0-based index); the translation is `sequence == dot - 1`. Each basis is correct on its own,
but crossing them is a silent off-by-one the type cannot catch: a 1-based dot tested with
`>=` re-owes the boundary event (a re-delivery), and a 0-based sequence tested with `>` skips
it (a gap). A consumer mixing `metis`-minted vectors with its own should make the basis
unrepresentable-to-confuse (a `Watermark(VersionVector)` newtype, or `next_sequence` /
`count_seen` accessors), not rely on remembering which `get` means what.
== Test map
Tests live under `src/metis/tests/`: `version_vector/`, `ideal/`,
`ideal_properties/`, `producer/`, `stability/`, `dot_set/`, `causal_store/`, `dot_fun/`, `node/`,
`composer/`, `purview/`, `retirement/`, `scope/`, `attest/`, `rhapsody/`, `studio/`,
`wire/`, `gate/`, and `fleet/` (the epoch protocol's end-to-end assurance rung,
xref:#fleet[below]), with shared generators
in `support.rs` and the inventory in `mod.rs`. `version_vector/`, `stability/`, `dot_set/`,
`causal_store/`, `dot_fun/`, `composer/`, `purview/`, `scope/`, and `attest/` are split into
examples and properties; `version_vector/examples/` is split by order, observation,
lattice, restriction/glue, and difference examples; `version_vector/properties/` is split by order, lattice,
restriction/glue, and residual-difference families; `composer/examples/` is split by
write-flow, exchange/adopt, and law-breaking store cases; `composer/properties/` is split by
facade/manual equivalence, coverage, and delta-exchange convergence laws; `causal_store/examples/` is
split by observed-remove flow, covered-pair/delta boundary, and `DotMap` disjointness
cases; `dot_fun/examples/` is split by multi-value register, keyed-register map, and
store-refusal recipes; `dot_fun/properties/` is split by checked covered fixture,
merge laws, read/restriction laws, and accessors; `dot_set/properties/` is split by exact-set, read/cut, restriction,
difference, and intersection families; `purview/examples/` is split by row/roster,
common-read, and owed/trust-boundary cases; `purview/properties/` is split by row, common-read,
and owed-targeting laws; `scope/properties/` is split by restriction, scoped vector,
scoped have-set/cut, and peek laws; `attest/examples/` is split by source/bridge,
lattice/residual, and absent-constructor probe examples; `attest/properties/` is split by
source constructors, lattice/order/residual, and view laws; `causal_store/properties/` is split by run convergence,
survivor-law merge, delta anti-entropy, restriction, and disjoint-batch
families; `rhapsody/` has `examples/` (shared builders in `mod.rs`, core sequence examples in
`core/` split by construction/dangling, order/run, and visibility/deletion cases,
`condense/` split by linear, branching, lifecycle, and hazard scenarios,
`visual/` split by anchor selection, child-index reads, backward runs, and reachability,
and specialized conformance examples in `conformance.rs`)
and `properties/` (the shared run model in `model.rs`, order oracle in `oracle.rs`, helper
re-exports in `mod.rs`, convergence/condense
laws split by fold, condense, and restriction under `convergence/`, and cached-order, child-index, reachability,
visual-insert, and backward-run laws split under `views/`). `causal_store/`
also carries `foreign/`, an out-of-tree `DotStore` conformance suite split into
`laws/` (checked covered harness, fixtures, axis laws, content laws) and register
recipes, plus a `tape.rs` replay helper; `rhapsody_convergence/tape/` is split into
the byte-tape driver, op semantics, reference-order oracle, wire oracle, and final convergence
assertions; `wire/have_set/examples/` is split by byte layout, frame prefix/version/length,
station canonicality, and run canonicality refusals; `wire/have_set/properties/` is split
by round-trip/canonical laws, parser totality, and shaped station/run refusals;
`wire/rhapsody/properties/` is split
by shared weave generation, round-trip/canonical laws, parser totality, dangling anchors,
and byte accounting; `retirement/` is examples-only,
and `studio/` is the composed collaborative-editor probe, xref:#studio[below] (its
editor harness is split into `editor/mod.rs`, `editor/text.rs`, `editor/cursor.rs`, and
`editor/gossip.rs`; its measurement report is split into `measurements/mod.rs`,
`measurements/readings.rs`, `measurements/output.rs`, `measurements/session.rs`,
and `measurements/probes.rs`; and its scenario suite into
`sessions/{text,cursors,gc,wire}.rs` with shared helpers in `sessions/mod.rs`);
`ideal/` is split by example family:
`delivery.rs`, `frontier.rs`, and `capacity.rs`; `ideal_properties/` is split by property family:
`delivery.rs`, `frontier.rs`, `evidence.rs`, and `capacity.rs`; `gate/` is split by invariant
family: `fifo.rs`, `quorum.rs`, and `laws.rs`; `producer/` is split into `examples.rs`,
`properties.rs`, and a local `support.rs`; `wire/` is split into `vector/` for the
`VersionVector` frame/parser examples and properties, `have_set/` for the `DotSet` run-length
frame examples and properties (PRD 0016), `rhapsody/` for the sequence-store frame examples
and properties, and `envelope.rs` for the `(Kairos, deps)`
envelope property. They
run under any feature set (the module is `no_std`, so they pass on `--no-default-features` too). The
invariant-to-test mappings are in
xref:../../docs/prd/0004-metis-causal-ordering.adoc#_invariants_and_their_tests[PRD 0004]
(the vector),
xref:../../docs/prd/0005-metis-causal-order-buffer.adoc#_invariants_and_their_tests[PRD 0005]
(the buffer), and
xref:../../docs/prd/0006-metis-event-producer.adoc#_invariants_and_their_tests[PRD 0006]
(the producer), and
xref:../../docs/prd/0011-metis-causal-stability-watermark.adoc#_invariants_and_their_tests[PRD 0011]
(the meet and the tracker), and
xref:../../docs/prd/0012-metis-dot-set-exact-have-set.adoc#_invariants_and_their_tests[PRD 0012]
(the have-set), and
xref:../../docs/prd/0013-metis-relative-base-change.adoc[PRD 0013]
(the relative reads, on both lattice types), and
xref:../../docs/prd/0014-metis-difference-reads.adoc#_invariants_and_their_tests[PRD 0014]
(the difference reads, on both lattice types), and
xref:../../docs/prd/0015-metis-causal-store-algebra.adoc#_invariants_and_their_tests[PRD 0015]
(the causal store algebra).
=== `VersionVector`
Property tests (proptest) pin the algebraic contract over a small station domain (so
vectors overlap and concurrency is frequent):
`prop_partial_order_reflexive_antisymmetric_transitive`,
`prop_merge_commutative_associative_idempotent`, `prop_merge_is_least_upper_bound`
(which also freezes `merge` as the pointwise max), `prop_concurrent_iff_incomparable`,
`prop_increment_dominates`, and `prop_absent_equals_zero`.
Example tests are split under `version_vector/examples/`: `order.rs` pins
happens-before, concurrency, and bottom cases; `observation.rs` pins canonical observation
and saturation cases; `lattice.rs` pins meet cases; `restriction.rs` pins base-change and
exact-glue cases; and `difference.rs` pins residual cases.
The S78 meet laws live beside the join laws they dualize:
`prop_meet_commutative_associative_idempotent`, `prop_meet_is_greatest_lower_bound` (the
glb characterization plus the pointwise-min freeze), and
`prop_join_meet_absorption_and_distributivity` (the vector order is a distributive
lattice, exercised in code), with named examples `test_meet_is_common_knowledge`,
`test_meet_bottom_annihilates`, and `test_meet_of_disjoint_pair_is_canonical`.
The S89 relative reads (PRD 0013) add their own laws: `prop_restrict_is_functorial`
(identity, idempotence, composition by roster intersection),
`prop_restrict_is_a_lattice_homomorphism_and_reflects_concurrency` (restriction commutes with
merge and meet and reflects concurrency, the one-way witness), `prop_sections_of_one_vector_glue_back`
(the sheaf condition: sections cut from one vector re-glue to it), and
`prop_glue_refuses_disagreement_with_the_first_witness` (the exact refusal beside the lax
`merge`), with named examples `test_restriction_creates_order` (the created-order hazard),
`test_restrict_to_empty_roster_is_bottom`, and `test_glue_refuses_what_merge_absorbs`.
The S95 difference read (PRD 0014) ships the adjoint ledger's residual section as law:
`prop_difference_is_the_co_heyting_residual` (the Galois connection, bottom iff dominated,
repay-to-join), `prop_difference_carries_claims_never_subtractions` (the pointwise freeze,
the shape trap as a property), `prop_difference_curries_and_preserves_debtor_joins`
(currying over creditors, debtor-join preservation, the co-Heyting exchange over the meet),
and `prop_difference_commutes_with_restriction` (the PRD 0013 R2 base-change witness), with
named examples `test_difference_is_the_claim_not_the_subtraction` (the ledger's shape
warning as a concrete pair) and `test_difference_bottom_identities`.
=== `Stability`
Properties pin the tracker's contract directly: `prop_watermark_is_the_meet_of_vouched_cuts`
(the watermark equals the n-ary meet of the members' join-folded reports, re-derived
independently of the tracker, and is a lower bound of each), `prop_watermark_never_regresses`
(monotone non-decreasing under any report sequence, the license to act on it), and
`prop_reports_are_order_invariant` (a report permutation yields the identical tracker, so
gossip reordering cannot change what is stable).
Example tests pin the named cases: `test_watermark_is_common_knowledge` (the pointwise min
across the roster, a partially-vouched station dropping out), `test_watermark_requires_every_report`
(an unreported member pins the watermark at bottom), `test_unknown_station_is_refused_unchanged`,
`test_stale_report_is_absorbed` (a late older report is join-absorbed),
`test_empty_roster_watermark_is_bottom` (the degenerate family answers bottom, never the vacuous
top), and `test_reports_reader_exposes_the_straggler`.
=== Departure (the `membership` suite, S336)
Fourteen pins in two halves. The tracker's doors: the freeze and its cure, the bound's four
properties (it reads the survivors and not the departing claim, it is readable in advance, it
only rises, it is bottom off the roster even when a survivor's cut carries that coordinate), the
two refusals, idempotence with watermark monotonicity, resurgence with the two directions in
which it falls short of a verdict (an in-flight report is a false positive, an epoch declaration
leaves no mark), the witness narrowing with the family (a per-station gate, so evicting the one
member that reported bare restores `watermark_cut` instead of freezing it forever), and the
re-declaration duty a rebuilt tracker imposes.
Then where departure stops: abandoning cures the watermark and deliberately leaves the epoch
rounds frozen (recoverably, nothing retired, the window intact), the two negative results
ruling out substitution, the roster-change refusal, and candidate-set stability under departure.
Every guard is mutation-verified.
The end-to-end companion is
`fleet::byzantine::abandoning_the_withholder_releases_the_meet_and_cures_this_freeze`: against
the fault R-83 named, releasing the meet is the whole cure, because a withholder of stability
reports leaves both epoch rounds supplied. Reasoning in
xref:../../docs/metis-membership-departure.adoc#where-departure-stops[the departure note].
=== The departure round (the `departure` suite, S339)
Twenty-four pins in three halves. The round's own doors: the bound is the survivors' join, the fence
holds at the proposal and becomes a verdict at the agreed bound, it speaks for one coordinate,
`Ragged` refuses a holding above its own floor and redelivery cures it, `FenceBroken` refuses a
raised promise, the departing station has no voice at any door, and proposals absorb without
regressing. The tracker door: only the attested one supplies a coordinate, the agreed bound is
latched (`Reattested`), and both of `abandon`'s refusals are inherited. Then the rounds the
attestation completes: the payoff against `membership`'s frozen control, the sealed join carrying
the agreed coordinate, the bound as a bar the watermark must still clear (so a departure licenses
only consignable records), the unconditional substitution over a departed member's own testimony,
the recovering-evictee race, and the reach that stops at one coordinate. Every guard is
mutation-verified.
The end-to-end companions are in `fleet::byzantine`:
`attesting_the_silent_members_departure_carries_the_fleet_through_the_seal` (the fault S336 left
uncured, cured through seal, consignment, and the certifiable grade),
`a_departed_member_that_speaks_again_is_refused_at_the_fence` (the verdict),
`a_crash_between_the_promise_and_the_seal_does_not_lower_the_fence` (the durability of the
promise), `two_departures_survive_a_restart_in_the_order_they_were_agreed` (the checkpoint carries
what it has sealed), `a_departing_members_native_traffic_does_not_ride_the_seal` (the successor
plane's fence), `successor_traffic_minted_before_the_round_seals_is_still_refused` (the honest
schedule that would otherwise wedge one generation later), and
`successor_traffic_folded_before_the_eviction_blocks_it_rather_than_wedging` (its dual, blocked for
one boundary rather than forever). Charter in
xref:../../docs/prd/0026-metis-membership-departure-round.adoc[PRD 0026].
=== `DotSet`
Properties check the compact representation against a plain reference set:
`prop_dot_set_is_an_exact_set` (membership agrees with the model; any insertion order yields a
structurally equal value), `prop_merge_is_the_union_join` (membership-exact, commutative,
associative, idempotent), `prop_floor_is_the_greatest_contained_cut` (gap-free and maximal),
`prop_high_water_is_a_join_homomorphism_and_floor_is_lax` (the asymmetric adjoint laws),
`prop_holes_are_exactly_the_missing_dots`, `prop_floor_and_high_water_bracket_and_never_regress`,
and `prop_from_witnessed_embeds_the_cut`. The PRD 0016 repair reads (S98) add
`prop_holes_for_is_the_whole_set_filtered` (the per-station view equals the whole-set holes
filtered to the station) and `prop_hole_count_equals_holes_counted` (the norm equals
`holes().count()`, computed without enumerating a gap). The S89 base change (PRD 0013) adds
`prop_restrict_is_the_fiber_selection` (restriction keeps exactly the roster's fibers) and
`prop_restrict_commutes_with_every_read_and_fold` (the exactness the vector's floor law gives up).
The S95 difference read (PRD 0014) adds `prop_difference_is_the_exact_owed_set` (the model
law plus strict ascending order), `prop_difference_repays_to_the_union` (serving the owed
dots reconstructs the merge; nothing owed iff subset),
`prop_holes_and_exceptions_are_difference_reads` (both shipped asymmetries as special
cases), `prop_cut_difference_enumerates_the_residual_spans` (the bridging law to the vector
residual), and `prop_difference_commutes_with_restriction` (the base-change witness). The
S96 intersection (PRD 0015 R9) adds `prop_intersect_is_the_meet` (membership-exact, the
connective laws) and `prop_floor_is_exact_and_high_water_lax_on_intersections` (the adjoint
ledger's mirror square plus `from_cut` meet-preservation, predicted before the operation
existed), with `test_dot_set_intersect_names_the_common_dots` the named audit example
(in `tests/causal_store/examples.rs`, beside its caller).
=== The causal store (`Dotted`, `DotMap`, `DotStore`)
The simulation is the reference model: random multi-replica histories of adds (through
the real `next_dot` write flow), observed removals, and gossip, replayed against a
global oracle of assigned and superseded dots. `prop_replicas_converge_to_the_oracle`
pins system-level convergence (any fold order; store exactly the oracle's survivors;
context exactly everything assigned; every replica absorbed),
`prop_merge_is_a_semilattice_join` the algebraic laws over run-reached states,
`prop_survivor_law_is_exact` the per-dot survivor law at the bare-store level,
`prop_projections_split_knowledge_from_survival` the deliberately-non-product split
(context exactly the knowledge join; store at or below the union), and
`prop_restrict_commutes_with_merge` the base-change witness (PRD 0013 R2). Named
examples pin the field failure modes:
`test_removal_does_not_resurrect_through_a_stale_peer`,
`test_concurrent_add_survives_concurrent_removal` (add-wins as delta observation),
`test_next_dot_survives_removal` (the doomed-dot trap),
`test_try_new_refuses_the_uncovered_pair` (the boundary witness),
`test_key_vanishes_when_every_dot_is_superseded` and
`test_nested_composition_removes_at_the_leaf` (canonical composition at depth), and
`test_write_flow_lands_the_dot` (the documented write recipe end to end).
Example tests pin the named cases: `test_floor_is_gap_free_and_maximal`,
`test_out_of_order_arrival_converges` (filled disorder leaves no trace),
`test_dot_zero_is_not_a_dot`, `test_duplicate_insert_is_idempotent`,
`test_hole_fill_absorbs_the_parked_run` (the compaction step),
`test_from_witnessed_round_trips`, `test_merge_fills_each_others_holes` (the strict lax case),
`test_high_water_matches_the_horizon_shape` (the cross-repo `{1, 6} -> 6` example),
`test_reports_honestly_for_stability` (the floor feeds `Stability::report`; no hole ever sits
below the watermark), `test_difference_names_the_owed_dots` (the mixed prefix-and-exception
serve list, then convergence), and `test_cut_difference_is_the_residual_span` (the dot-level
face of the claims-not-subtractions example).
The foreign-store conformance suite (`tests/causal_store/foreign/`) exercises the axis
against an out-of-tree register store beside the shipped instances:
`prop_dot_set_conforms_to_the_axis`, `prop_dot_map_conforms_to_the_axis`,
`prop_inscribed_conforms_to_the_axis`, and `prop_inscribed_content_follows_the_dot` (law 3,
the per-impl obligation a generic harness cannot reach).
=== `DotFun`
Properties pin the value-carrying survivor law and the axis conformance:
`prop_survivor_law_is_exact_with_values` (the per-dot survivor law at value granularity),
`prop_causal_merge_is_commutative`, `prop_causal_merge_is_associative`,
`prop_causal_merge_is_idempotent`, `prop_bottom_is_the_identity`,
`prop_novel_to_selects_the_unseen_dots`, `prop_restrict_commutes_with_merge`,
`test_default_is_bottom`, `test_iter_and_values_are_ascending_by_dot`, and
`test_len_and_is_empty_track_the_dots`.
Example tests pin the named cases: `test_dot_zero_insert_is_refused`,
`test_duplicate_dot_insert_is_refused_unchanged` (content is never reassigned),
`test_singleton_of_dot_zero_is_empty`, and the register recipes over `Dotted<DotFun<V>>`:
`test_register_concurrent_writes_are_siblings`, `test_register_write_supersedes_observed`,
`test_register_observed_clear_empties_without_resurrect`,
`test_register_folds_converge_in_both_orders`, `test_keyed_register_map_writes_and_clears_per_key`,
and `test_keyed_register_map_key_vanishes_when_last_dot_superseded`.
=== `Node`
The axis conformance runs beside the other instances
(`prop_node_conforms_to_the_axis`, in `causal_store/foreign/laws/axis.rs`, over seeds
that exercise all four components). The node's own properties (`tests/node/properties/`)
pin fleet convergence over generated write/re-kind/retract/gossip tapes
(`prop_fleet_converges_under_full_exchange`), re-kind atomicity at any synced peer
(`prop_rekind_is_atomic_at_any_synced_peer`), and the kind reads against an independent
reference recomputation (`prop_kind_reads_match_the_reference`).
Example tests (`tests/node/examples/`) pin the named cases: the cross-component straddle
refusals (`test_a_dot_lives_under_exactly_one_component`,
`test_component_refusals_pass_through`), canonical drop at node grade
(`test_a_bottom_node_vanishes_from_its_parent_map`), the kind reads
(`test_kinds_present_reads_tag_claims_and_shaped_content`,
`test_sole_refuses_a_plural_node_with_the_witness`,
`test_no_evidence_reads_none_and_residue_is_not_evidence`), the emptiness verdict
(`test_a_tag_only_node_is_an_empty_node_of_its_kind`), the one-covered-delta
reassignment and its concurrency half
(`test_a_kind_reassignment_is_one_covered_delta_with_no_window`,
`test_a_concurrent_edit_survives_a_reassignment_and_surfaces`), the caller-built-depth
exhibit (`test_a_deep_caller_built_tree_merges_and_reads`), and the shaped
counterexamples the store-algebra note cites
(`test_a_sum_shaped_merge_cannot_keep_the_survivor_law`,
`test_an_exclusive_kind_merge_discards_a_concurrent_subtree`,
`test_slots_alone_cannot_say_conflict_but_the_node_must`).
=== `Scholia` and the extent read
The axis conformance runs beside the other instances
(`prop_scholia_conforms_to_the_axis`, over seeds spanning every verge shape). The
projection laws live with the rhapsody suites: `prop_extent_agrees_with_the_positional_oracle`
(every verge pair against an independent positional oracle over enriched
sided-and-tombstoned histories, with the covered-is-a-contiguous-interval arm) and
`prop_edge_inserts_respect_the_sides` (the sided expansion law), in
`tests/rhapsody/properties/views/extent.rs`; the verdict examples (covered, empty,
sided edges, tombstone boundaries, dangling, condense-excision dangle, inverted, the
overlap derivation) are `tests/rhapsody/examples/extent.rs`. The store flows
(`tests/scholia/examples.rs`): the shared-mark lifecycle
(`test_a_shared_mark_converges_edits_and_retracts`), the marks-beside-text integration
(`test_marks_ride_identity_through_concurrent_text_edits`), and the retention pin set
(`test_anchor_dots_reads_the_pin_set`).
=== `Metatheses` and the recension read
The axis conformance runs beside the other instances
(`prop_metatheses_conforms_to_the_axis`, in `tests/causal_store/foreign/laws/axis.rs`,
over seeds whose testimonies are deterministic functions of the dot). The replay laws live
in `tests/metathesis/properties.rs`: `prop_recension_converges_and_matches_the_reference`
(every replica's order, refusals, and pending set agree with each other and an independent
replay oracle computed from public reads alone, over insert/delete/move/undo/gossip
histories, plus the empty-record identity) and `prop_no_moves_means_no_refusals`. The
flows (`tests/metathesis/examples.rs`): 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 by retract
(`test_undoing_a_move_by_retract_restores_the_birth_order`), the tidy re-move
(`test_a_re_move_supersedes_tidily`), marks over moves (`test_marks_follow_moved_content`),
and the out-of-order surfaces (`test_a_pending_move_surfaces_and_resolves`,
`test_moving_a_tombstone_carries_its_subtree`). The collation's laws and pins (S203)
live in `tests/metathesis/collation/`, mapped in the rhapsody note's test map.
The design-only epoch boundary has its bounded falsifier in
`tests/epoch_refound/` (S213): `test_anchor_support_matrix_exposes_the_annex_boundary`
runs both fold orders across live/swept anchors and position-only/annex translation;
`test_equal_rank_rechaining_changes_live_anchor_context` isolates the
incumbent-sibling condition after exercising the full sided fallback; and
`test_rechaining_changes_a_move_refusal_even_with_the_annex` proves the annex cannot
preserve the exact law once re-chaining changes the effective ancestor relation; and
`test_replay_order_decides_which_cycle_former_is_refused` makes a reverse-arrival
three-move cycle obey both halves of the production `(rank, testimony dot)` order,
including the all-ranks-equal testimony tie-break. The S215 extension models the
charter's chosen shape, the sealed-stratum shadow (PRD 0024), as the maintained
`Shadow` beside the eager `judge`, under a dot map frozen at declaration
(live-at-cut compaction by walk order, the affine shift above the ceiling):
`test_the_shadow_restores_the_swept_anchor_bucket_order` and
`test_the_shadow_preserves_the_old_world_move_verdict` pass both S213 falsifiers
through the shadow (commutation restored, both arrival orders, fast path and
rebuild); `test_the_shadow_carries_equal_rank_rechaining` closes the equal-rank
arm; `test_a_window_arrival_re_decides_a_record_move` proves the shadow must
carry the movement record, not just the effective state (a lower-keyed window
arrival retroactively flips a record move's verdict);
`test_an_unwitnessed_cut_lets_a_delayed_tombstone_shift_the_identity_plane` is
the R1 seal falsifier (readings converge, identities never do);
`test_window_born_chains_survive_the_affine_shift` pins consecutive-dot
preservation under a frozen map; and
`prop_the_boundary_holds_reading_equality_at_every_split` is the R4 generated
law (the boundary crossed at every split of a generated history, EVERY causal
arrival order exhaustively, the history bounded to five deltas exactly so the
enumeration never samples; exact agreement with the eager judgment at every
prefix in reading, decisions, and the projected identity sequence, under a
frozen map whose live compaction is cross-checked per split against
`refound`'s independent walk-order rule, with injectivity over the whole
projection). The
prototype remains the bounded exhaustive oracle for the production
`EpochShadow` suite (S219). The production fold it first oracled landed as
`Rhapsody::refound` (S216, PRD 0024
stage one), pinned in `tests/refound.rs`:
`assert_fold_laws` is the one-place law bundle (order preservation through
the frozen map, injective per-station compaction into `(s, 1..=n_s)`,
floor-perfect recording state, tombstones refused by the map, the affine
half at each ceiling, and determinism twin-fold equality), exercised by
the deterministic bake/sweep example, the born-coalesced explicit-entry
pin, the head-grade fixed-rule spelling pin
(`test_refound_heads_spell_the_fixed_public_rule`: a station segment's
head anchors after its walk predecessor and carries the per-station base
rank, never a rank derived from another station's chain;
mutation-verified against the always-chain mutant, S217), the
`UnsealedStratum` refusal pair, the empty-store identity, and
`prop_refound_preserves_the_effective_order` over generated documents
(weaves at either side, deletions, and applied, superseded, and refused
movements through the real pair and clocks). The fold's identity
arithmetic is itself the third dual-homed Creusot core
(`rhapsody/refound/pure.rs`, S217): the sampled bundle cross-checks the
proven contracts end to end.
=== `Composer`
Properties pin the facade against the manual flow: `prop_scribe_matches_the_manual_flow` (the
one-call `compose` equals the hand-rolled read-build-merge flow), `prop_every_returned_delta_is_covered`
(every delta the facade emits covers its own store), and `prop_delta_exchange_converges_like_full_states`
(shipping `owed_to` deltas converges replicas exactly as exchanging full states).
Example tests pin the named cases: `test_compose_assigns_the_first_dot_and_holds_it`,
`test_compose_calls_ascend_strictly`, `test_compose_that_supersedes_is_covered`,
`test_compose_super_equals_the_manual_read_then_compose` (the TOCTOU close),
`test_compose_receipt_is_the_merged_dot_even_with_a_merge_around_the_call` (the receipt footgun
close, S112), `test_compose_over_a_lying_store_rides_the_lie_through` (the unreachable refusal
arm), `test_absorb_learns_a_peers_delta`, `test_retract_and_owed_deltas_are_covered`,
`test_adopt_round_trips_and_continues_fresh`, and
`test_compose_after_retracting_everything_stays_fresh`.
=== `Purview` and `Received`
Properties pin the lower-bound tracker: `prop_rows_never_regress`,
`prop_rows_are_evidence_order_invariant`, `prop_received_rows_stay_lower_bounds` (the safety
direction), `prop_common_is_the_intersection_and_never_regresses`,
`prop_common_floor_is_the_floor_of_common`, `prop_owed_is_delta_for_against_the_row`, and
`prop_owed_delta_converges_like_the_full_state`.
Example tests are split under `purview/examples/`: `rows.rs` pins roster and row-update
cases, `common.rs` pins common-context reads, and `owed.rs` pins owed-delta targeting plus
the under/over-claim trust boundary. The `compile_fail` doctest in the `Purview::note`
rustdoc pins that a bare `DotSet` no longer notes.
=== `Retirement` and `Retired`
Examples-only (the tracker is a thin meet over acknowledgements):
`test_retired_is_the_meet_across_the_roster`, `test_retired_requires_every_member`,
`test_retired_is_monotone_non_decreasing`, `test_acknowledge_is_order_invariant`,
`test_stale_acknowledgement_is_absorbed`, `test_unknown_station_is_refused_unchanged`,
`test_empty_roster_retired_is_bottom`, `test_acknowledged_reader_exposes_the_laggard`, and
`test_trust_is_the_audited_escape`. The `Retired` rustdoc carries a `compile_fail` doctest (a
bare `DotSet` cannot `condense`) beside a passing witnessed-path example.
=== `Cut` (the `attest` suite)
Properties are split under `attest/properties/`: `sources.rs` pins every honest-source
constructor as a genuine cut, `lattice.rs` pins closure, order, and residual laws, and
`views.rs` pins the one-way exits.
Example tests are split under `attest/examples/`: `sources.rs` pins source and adoption-bridge
cases, `lattice.rs` pins order, residual, restriction, and bottom cases, and
`construction_probes.rs` pins absent `Default` / `From<VersionVector>` construction doors.
The four absent-door `compile_fail` doctests live in the `Cut` rustdoc.
=== The epoch lifecycle (`Epochs`, `tests/epoch/`)
The stage-two mandatory pins (PRD 0024 R5/R6), each mutation-verified
against a lone mutant of the machine (winner rule flipped, coverage check
dropped, recognizer flipped, truncation dropped, all KILLED, S218):
`the_concurrent_declaration_race_fixes_one_winner_everywhere` (the R5 race:
two declarers, different cuts, all 6! orders of the five decision events and
the stability sync per replica over an honest fabric with gossip
redelivery; one fixed-rule winner everywhere, the loser surfaced until the
seal, byte-identical sealed records), `adoption_waits_for_the_confirmation_watermark`
(the R5 guard isolated: all confirmations folded, watermark short of the
join, adoption refuses `Unconfirmed`; covered, it fixes and adopts),
`a_causally_later_declaration_is_refused_while_the_window_is_open` (the
deterministic `WindowOpen` refusal), `a_declaration_needs_the_watermark_witness`
(the R1 license: one bare report withdraws it),
`a_witnessed_watermark_must_rise_to_the_declared_basis`,
`a_bottom_basis_licenses_the_first_epoch`, and
`an_unrisen_peer_declaration_refuses_identically_everywhere` (the R1 risen
half, ruling R-40/S222: both doors refuse `Unrisen` below the
caller-declared basis with the first uncovered station as evidence,
coverage inclusive, the empty basis lawful; three lone mutants, either
door's check dropped and the strict-coverage flip, all KILLED),
`the_sealed_join_is_the_duplicate_recognizer` (covered dots absorb
identically on every ask, uncovered are the typed `AddressMiss`, window
traffic routes to the shadow, post-seal duplicates of the declaration and
both report kinds absorb), and `the_lineage_holds_the_horizon_and_refuses_below_it`
(retention at exactly `k`, `BeyondHorizon` exact at the boundary, a
never-sealed address indistinguishable and identically refused). The
reads-across-the-seal half of the R6 duplicate law is pinned with the
stage-three shadow below.
=== The epoch boundary (`EpochShadow`, `tests/epoch_shadow/`)
The production stage-three pins are
`the_shadow_preserves_the_old_world_cycle_verdict` and
`the_shadow_keeps_a_swept_anchor_bucket_in_both_arrival_orders` (both S213
falsifiers through the real store and recension),
`an_earlier_window_move_redecides_the_retained_record` (the shadow owns the
record, using lawful above-cut testimony dots),
`a_swept_at_cut_identity_is_refused_before_mutation` and
`a_novel_below_cut_testimony_is_refused_before_redecision` (novel identities
in either pair are rejected before mutation while covered replays absorb),
`above_cut_state_cannot_shift_the_frozen_map`
(two replicas must start from the same cut-bounded stratum; above-cut births
then converge through either delivery order),
`projection_agrees_with_eager_judgment_at_every_prefix` (R4, generated real
histories, decisions and identities),
`native_events_wait_for_exactly_the_adopted_declaration` (winner-only native
gate and typed competing-adoption refusal), and
`duplicate_delivery_reads_identically_across_the_seal` (the R6 half stage
two deliberately deferred).
`only_winner_adoptions_seal_and_loser_replays_absorb` is the stage-three
review's repair pin across the lifecycle seam: loser-addressed adoption
reports cannot complete the winner's round, and after seal every retired
candidate declaration and report absorbs without reopening a window or
blocking the next declaration.
`peer_reports_cannot_seal_before_local_adoption` proves even a complete,
covered winner round cannot close the window before this replica obtains its
opaque `Adopted` witness.
`a_peer_declaration_causally_after_the_window_is_never_a_candidate` pins the
candidate antichain in forward and reverse arrival order, and
`an_incomplete_below_cut_stratum_is_refused` pins structural completeness of
the fold input.
`a_novel_below_cut_tombstone_cannot_activate_a_window_child` pins validation
of invisible recording state. `a_declaration_address_must_be_fresh_above_its_cut`
and the generation-reuse arm of `the_lineage_holds_the_horizon_and_refuses_below_it`
pin declaration freshness without old/new aliasing.
`off_roster_declarations_cannot_enter_the_window` pins declaration membership;
`confirmation_must_cover_the_declaration_address` pins receipt evidence before
the confirmation round can advance.
The stage-four pins (S263, ruling R-50) sit beside them.
`a_verbatim_anchor_carry_flips_a_rank_contest_the_consignment_preserves` is the
third S213-class falsifier (re-based sibling ranks flip an honest window
birth's bucket contest, so only the judged outcome crosses);
`the_old_world_move_verdict_crosses_baked_never_as_testimony` passes the
first falsifier through the seal itself.
`the_consignment_carries_births_moves_and_deletes_whole` pins the carry classes
and the shared gap-free context;
`the_consignment_reads_identically_in_both_arrival_orders` and the generated
`any_window_braid_consigns_the_projection_exactly` pin path-independence,
byte identity, and the structural context translation against its per-dot
reference. The refusals each have a pin (`a_foreign_seal_cannot_consign`,
`an_unfoldable_window_is_refused_at_the_consignment`,
`post_seal_traffic_cannot_enter_the_consignment`), with
`a_seal_covering_a_withheld_delta_refuses_then_the_delivery_cures` proving
the handed-back shadow completes after the missing delivery.
`a_displaced_provisional_declaration_stays_in_the_seal_record` and
`an_above_join_refused_declaration_never_contaminates_the_consignment` pin the
protocol ledger's two faces (receipt-time recording, join
canonicalization); `a_window_dead_birth_crosses_as_context_only`,
`a_dead_at_cut_identity_does_not_cross_the_consignment`, and
`a_ceiling_image_does_not_overflow_the_chain_guard` pin the identity
classes and the checked-adjacency boundary; and
`a_window_move_can_flip_a_native_move_verdict_hence_the_deferral_duty`
records why the recipe defers native movement testimonies to the seal.
[#fleet]
=== The fleet (`tests/fleet/`, S220, ruling R-39)
The epoch protocol's end-to-end assurance rung: a deterministic,
seed-replayable fleet of full-stack replicas (causal pairs, `Stability`,
`Epochs`, stratum rebuild, `EpochShadow`, `EpochIdeal`, seal) under an
adversarial fabric (`fabric.rs`: seeded schedule, reordering, one-shot
duplication, bidirectional severance). `replica.rs` is the executable
consumer recipe (dotted deletes, event-dot have-sets, the declare-time
dry-run, the log rebuild, the seal taking `EpochShadow::consign` as the
next generation's base since S263 under ruling R-50, with every seal
pinned to open on the frozen projection and native movement testimonies
deferred to the seal by duty, and, since S223 under ruling
R-41, the retirement round: cut-gated acknowledgements, the fleet-applied
condense claim, testimony-anchor pins, generation-scoped evidence); its
module note records why each duty is load-bearing. The scenarios pin the honest single-boundary crossing
with window births, deletes, moves, and gated native traffic
(`the_honest_fleet_crosses_one_boundary_and_converges`), the carry itself
across two boundaries with laggard births and moves in flight
(`window_births_and_moves_cross_the_seal_alive`), concurrent
declarations (`competing_declarations_fix_one_winner_everywhere`), the R8
liveness freeze (`a_silent_member_freezes_the_seal_until_it_heals`), and the
two-epoch lineage with horizon truncation
(`two_epochs_advance_the_lineage_and_the_horizon_truncates`), and the whole
hygiene arc with exact excision counts
(`the_hygiene_lifecycle_pins_excises_and_crosses_the_boundary`: pin, excise
the target, retract dotted, unpin, excise the anchor, duplicate re-learn
and re-excision, then across a seal onto a fresh tracker). `boundary/`
carries the discipline counterexamples
(`an_undotted_retraction_cannot_be_classified_at_the_boundary`,
`a_witnessed_cut_can_still_refuse_the_stratum`,
`the_have_set_counts_events_never_context_spillover`, the converse
direction: a context-only sighting must not raise the watermark past an
undelivered weave, and the S223 retirement four:
`a_retirement_acknowledgement_counts_only_when_its_cut_is_delivered`,
`a_weave_racing_a_partial_condense_strands_its_anchor` (the arm's
principal finding: the visual-insert rule anchors through tombstones by
design, so an honestly gathered meet cannot license excision while writes
flow; the claim must be fleet-applied first, epoch-shaped coordination in
miniature),
`an_undotted_testimony_retirement_cannot_be_classified_at_the_boundary`
(identical contexts and cut, divergent frozen maps: the movement-plane
twin, whose live shape is the future undo path; the orphaned-target case
is boundary-neutral), `retirement_evidence_is_generation_scoped` (the
compacted plane recurs numerals), and `an_outrun_testimony_is_not_an_orphan`
(orphanhood is removal evidence, target-in-context beside locus-gone,
never locus absence alone: the review-caught hazard)), and `properties.rs` runs
the generated laws (`any_schedule_seals_two_epochs_and_converges`: two full
lifecycles under any tape and schedule, optional whole-window severance,
identical lineages, projections, pairs, and wire bytes at quiescence; its
persisted regression seed also pins the parked-note strand the harness
found; and `any_schedule_with_condense_and_hygiene_converges`: mixed edit
and retirement tapes with fleet-applied condense points whose per-replica
excision counts must agree, a boundary crossing, and a third-generation
tape). Four S223 lone mutants (the acknowledgement gate dropped, the
seal-time tracker reset dropped, the anchor pin dropped, the
removal-evidence test dropped) are each KILLED at their named assertion. Old-plane births and moves are judged through the shadow and
asserted at the seal but deliberately not carried into the next generation's
native store: that carry is PRD 0024 stage four, gated on the first adopting
consumer.
=== `Scope`
Properties pin the preservation law and the fold homomorphisms:
`prop_scoped_order_preserves_global_order`, `prop_concurrent_globally_reflects` (the escaping
verdict), `prop_scoped_restrict_agrees_with_unbranded`, `prop_restrict_all_matches_pointwise_restrict`,
`prop_scoped_vector_folds_commute_with_restriction`, `prop_scoped_dot_folds_commute_with_restriction`,
`prop_map_keeps_the_brand_and_applies_the_closure`, `prop_floor_cut_agrees_with_forget_then_floor_of`,
and `prop_peek_agrees_with_forget`.
Example tests pin the named cases: `test_created_order_hazard_through_the_scope` (the order
verdict sound only over the roster) and `test_concurrency_reflects_globally_through_the_scope`.
The cross-scope non-unification (same roster, different invocation) and the no-escape and
forget-then-escape rules are pinned by `compile_fail` and passing doctests in the `scope`
rustdoc, the type-level proof obligations the brand exists to enforce.
[#studio]
=== The studio probe
The studio (`tests/studio/`, S110) is the composed reference model, where every epoch
surface meets: a `Dotted<Rhapsody>` document edited by `Composer` writers, cursors as
`DotFun` registers, gossip targeted by `Purview` and GC bounded by `Retirement`, driven
through real deltas and measured. It is the crdt-vision's measurement bench, so its
`measurements_report` emits the delta-byte and residue figures the staged arcs pin their
firing signals to. Example sessions: `test_two_writers_interleave_words`,
`test_concurrent_edit_and_delete_of_a_word`, `test_cursors_converge_as_registers`,
`test_typing_burst_with_laggard`, `test_gc_bounds_the_session`,
`test_gc_residue_is_anchored_tombstone_chains`, and `test_wire_round_trip_of_a_session_snapshot`.
The block-document probe (`tests/studio/blocks/`, S186; PRD 0019 stage A under ruling
R-16) is the structured sibling: a `Page` of four causal pairs (block order as a
`Rhapsody` of block dots; fields as `DotMap<BlockDot, DotMap<Field, DotFun<&str>>>`;
paragraph content as `DotMap<BlockDot, Rhapsody>`, the first in-tree `Rhapsody`-under-map
composition; table content as nested maps) with a read-side conjunction render that
classifies every cross-pair delivery state (`Rendered`). Its scripts record the stage-A
evidence ruling R-17 reads: `coherence.rs` (the conjunction rule suffices for non-empty
traffic; ghost and kind-pending classified, the orphan silent, the empty block the
recorded limit, since absence cannot say "empty"), `kinds.rs` (concurrent kinds surface as
siblings; the stale-subtree and atomic-reassignment findings that fired stage B),
`move_fork.rs` (the identity-fork exhibit, stage C's number), and `measurements.rs`
(`blocks_report`, the block-shape counters: per-edit delta shapes, conjunction lookup
costs, key-space duplication, anomaly windows per interleaving, the container-local tree
viewport).
=== `Ideal`
The properties feed a *valid-history generator* (`build_history`, `tests/support.rs:67`): a small
simulation where each station is a real `Producer` that `observe`s some peers' events, then
`produce`s one. Driving the shipped send step rather than a parallel re-implementation
makes this an end-to-end test of producer output: the generated `(stamp, deps)` pairs form
a real causal execution, the full closure of every event is present, and `a -> b` implies
`a.stamp < b.stamp`. Each property feeds the buffer a `prop_shuffle`-d permutation of one
history:
* `prop_release_respects_causality` (R2): every released event is deliverable against
the events already released.
* `prop_every_event_released_once` (R5): the full closure releases each event exactly
once and `pending` empties.
* `prop_duplicates_dropped` (R5): inserting every event twice still releases each once.
* `prop_release_order_is_permutation_invariant` (R4): two arrival permutations release
in the same order.
* `prop_concurrent_frontier_in_kairos_order` (R4): each release is the `Kairos`-minimal
among everything deliverable at that moment.
* `prop_pop_ready_releases_frontier_minimum` (R4): the `frontier` reader agrees with the
default, its `Kairos`-minimal is exactly what `pop_ready` releases, and it is empty
exactly when nothing is ready.
* `prop_frontier_members_are_pairwise_concurrent` (R4): every member of the ready
frontier is pairwise concurrent with the others (a genuine antichain).
* `prop_pop_ready_event_exposes_causal_evidence` (S32b): every witness `pop_ready_event` returns
contains an event deliverable against the merge of the events released before it, recomputed
purely from the returned `(stamp, deps)`, so the linearization carries its own causal
justification.
Example tests pin the named cases: `test_chain_across_two_stations` (effect inserted
before cause), `test_concurrent_pair_released_in_kairos_order`,
`test_gap_blocks_then_fills`, `test_stale_replay_dropped`,
`test_frontier_is_the_ready_antichain` (the ready set is the concurrent pair and feeds
`pop_ready` its minimum), `test_frontier_empty_when_blocked` (a gap empties the
frontier), `test_pop_ready_event_carries_stamp_and_deps` (the full-event reader hands back the stamp
and deps `pop_ready` drops, and the causal order is recoverable from them), and the release-witness
tests (the gate brand is zero-storage, formatting does not constrain the marker, and the occurrence
returned is the one folded into progress).
The bounded `try_insert` (S30) adds four: `test_try_insert_buffers_below_capacity` (under the
bound it behaves like `insert`), `test_try_insert_rejects_at_capacity_unchanged` (a full backlog
hands the event back and leaves the buffer unchanged), `test_try_insert_drops_stale_without_consuming_capacity`
(a stale replay is dropped, not rejected, and never spends a slot), and
`test_try_insert_reclaims_dead_twin_when_full` (a full insert prunes a lingering pre-delivery
duplicate before rejecting, so a live event still buffers). S31b adds the bound invariant as a
property, `prop_try_insert_never_exceeds_capacity` (after every `try_insert` the live backlog
never exceeds `capacity`, and a rejection hands the event back), and pushes the bounded path
through the non-causal gates (`test_try_insert_fifo_rejects_at_capacity`,
`test_try_insert_quorum_is_a_hard_cap`, the latter proving a trivial-`stale` gate reclaims
nothing).
=== Gate seam (`Fifo`, `Quorum`, `And`)
The non-causal gates exercise the same machine: `test_fifo_has_no_cross_source_dependency` (a
source delivers despite another's gap, the behavior causal completeness forbids),
`test_fifo_orders_concurrent_sources_by_kairos` (the gate-independent linearization breaks the
tie), `test_fifo_drops_stale_replay`, and `prop_fifo_releases_each_source_in_seq_order` (each
source comes out `1..=count` whatever the arrival order). The test-only `Quorum` gate
(`test_quorum_gate_releases_on_threshold`) proves the seam carries a non-causal threshold rule,
release once enough distinct stations have contributed, on the same `Ideal`.
`test_and_holds_back_until_both_gates_admit` composes that caller-shaped gate with `Causal` and
pins the dynamic rule that both component progresses advance only on a genuine product release.
`test_and_progress_uses_the_product_order` protects the nominal progress type's comparable and
crossed cases.
The stale-terminality contract (R1, xref:../../docs/metis-gate-stale-contract.adoc[the
gate-stale-contract note]) is pinned by the exported dependency-free `check_gate_laws`, which
checks one caller-generated ascending progress pair for monotone `advance`, terminal `stale`,
disjointness from `deliverable`, and the joint up-set, the last an independent law rather than a
derived consequence (amended S337). Descending and incomparable pairs
are typed fixture failures. The property suite instantiates it for the leaf gates, the test-only
threshold, their product, and the externally opened epoch gate over its reachable progress pairs
(`prop_causal_gate_is_terminal`, `prop_fifo_gate_is_terminal`,
`prop_quorum_gate_is_terminal`, `prop_and_gate_is_terminal`,
`prop_epoch_gate_is_terminal`); adversarial fixtures pin every error variant. Generator strategy
and the dynamic released-only proof stay outside the checker. The
`prune_stale` `debug_assert` checks disjointness at runtime in debug builds.
=== `Producer`
Properties pin the send/receive contract directly: `prop_produce_is_self_contiguous` (each
produce advances the sender's own dot by exactly one), `prop_produce_deps_are_closed` (a
produced `deps` equals the post-increment knowledge and dominates every observed event's
deps), `prop_produce_stamp_dominates` (a produced stamp exceeds every observed stamp, the
high-water now held in the clock), `prop_observe_is_order_invariant` (observing a set in any
permutation yields the same knowledge, and a later produce dominates every observed stamp
regardless of order), and `prop_self_echo_is_safe` (re-observing own events leaves knowledge
unchanged and never breaks monotonicity).
Example tests pin the named cases: `test_successive_produces_are_monotonic` (every mint uses
`now`; each stamp exceeds the last), `test_observe_advances_knowledge_and_stamp` (learning
from one event raises knowledge and carries cross-station causality into the next stamp),
`test_self_echo_ticks_clock` (under frozen physical time, a self-echo's receive-rule tick
lands the next stamp one logical step higher, S21), `test_concurrent_first_events`
(independent first events are concurrent), and `test_producer_feeds_buffer_end_to_end` (a
real producer chain fed to a real buffer releases in causal order).
=== Wire encoding (PRD 0007)
Properties over `arb_vv()` (and `arb_kairos()` for the envelope): `prop_vv_bytes_round_trip`
(decode inverts encode, R6), `prop_vv_bytes_are_canonical` (a value built with redundant
zero-observes encodes identically, so byte-equality is value-equality, R2),
`prop_vv_from_bytes_never_panics` (arbitrary bytes decode to `Ok` or `Err`, never panic, and
an accepted frame re-encodes identically, R4), `prop_envelope_round_trips` (a
`(stamp, deps)` envelope survives concatenate-then-split-decode and the payload tail returns
untouched, R7), and `prop_envelope_from_prefix_never_panics` (the composed envelope decode is
total over arbitrary bytes: neither parser panics, an accepted frame re-encodes to the exact
bytes it consumed, and the tail is the untouched suffix; S85, the always-on twin of the
`envelope_from_prefix` fuzz target).
Example tests pin the named cases: `test_vv_to_bytes_layout` (the exact bytes for `{1:1, 2:5}`
and the empty vector, R1), `test_vv_from_bytes_rejects_unknown_version` (R3),
`test_vv_from_bytes_rejects_bad_length` (trailing bytes, a sub-header buffer, and a tiny frame
claiming `u32::MAX` entries rejected in `O(1)`, R4), `test_vv_from_bytes_rejects_zero_counter`,
and `test_vv_from_bytes_rejects_unsorted_stations` (unsorted and duplicate, R4). The
coverage-guided `fuzz/fuzz_targets/vv_from_bytes.rs` target drives the never-panic and
re-encode invariants past what proptest reaches.
=== Have-set wire frame (PRD 0016)
The `DotSet` run-length frame (S98) is tested in `tests/wire/have_set/` the way the vector
frame is. Properties over generated have-sets: `prop_have_set_bytes_round_trip` (decode inverts
encode) and `prop_have_set_bytes_are_canonical` (redundant insertion histories encode
identically, so byte-equality is value-equality); the totality trio
`prop_have_set_from_bytes_never_panics`, `prop_have_set_truncation_never_panics` (every prefix
length), and `prop_have_set_flip_byte_stays_total` (a flipped valid frame stays `Ok`/`Err`),
each also asserting an accepted frame re-encodes to its own bytes; and the shaped rejections
`prop_have_set_rejects_swapped_stations`, `prop_have_set_rejects_run_adjacent_to_floor`,
`prop_have_set_rejects_adjacent_runs`, and `prop_have_set_rejects_zero_length_run`, which break
exactly one canonical aspect of a valid frame. Example tests pin the layout and every rejection
variant by hand: `test_have_set_to_bytes_layout`, `test_have_set_empty_frame`,
`test_have_set_from_prefix_splits_the_tail`, and the `test_have_set_from_bytes_rejects_*` set
(unknown version, short input, empty station, non-ascending stations, zero-length run, a run
adjacent to the floor or to its predecessor, run overflow, and the dot-budget `run_too_long`).
The `fuzz/fuzz_targets/have_set_from_bytes.rs` target drives the never-panic and re-encode
invariants past the proptest, the decompression-bomb boundary the vector frame does not carry.
Since Polis S3 (`5d10141`) embeds v1 in its authenticated possession protocol,
`prop_polis_possession_have_set_never_panics` and the
`fuzz/fuzz_targets/polis_possession_have_set.rs` target also drive the exact-slice,
explicit-budget seam beneath the outer length and signature fields. Polis owns the complete
authenticated-frame target; this crate pins only its own canonical inner bytes and allocation
bound.