= Glossary
:toc: macro
:toclevels: 2
Minerva uses one project term for each concept. It models three distinct types
of time. Greek terms keep these types separate. Other documents use the terms
in this glossary.
An entry includes a classical source only when the source supports a type
boundary, API decision, or invariant. A source quotation must constrain the
meaning of the project term. Decorative quotations are out of scope.
toc::[]
== Mythological frame
[horizontal]
Minerva:: Roman goddess of wisdom (Greek Athena). The crate name. The thesis is
that ordering events well under concurrency is an act of practical wisdom, not
just bookkeeping. The myth is the module tree: Zeus made Mētis his first wife,
wisest among gods and mortal men, swallowed her on the counsel of Gaia and
Ouranos, and afterwards bore Athena from his own head (Hesiod, Theogony
886-900, 924); cunning carried inside wisdom, `metis` inside `minerva`. Ovid
supplies the Roman name's thesis line: _mille dea est operum_, "she is the
goddess of a thousand works" (Fasti 3.833), a library of many materials,
never one framework.
mētis (μῆτις):: Cunning, adaptive, practical intelligence; the wisdom to act
rightly _at the right moment_. The decision layer of the crate (see `metis` in
the target architecture); ships a version vector, a delivery buffer (the
order `Ideal`), a sender-side event producer, a cross-node stability
tracker, and an exact have-set (S10b, S14b, S15b, S78, S83). It _perceives_
concurrency and _delivers_ it safely; what it does not yet expose is the
_deinotēs_, the skill of resolving it (chartered in
xref:prd/0008-metis-deinotes-concurrency-resolution.adoc[PRD 0008]).
Two sources hold structural weight. Homer's maxim "by mētis, not force, is
the woodcutter far better" (μήτι τοι δρυτόμος μέγ᾽ ἀμείνων ἠὲ βίηφι, Iliad
23.315) is the layer's concurrency posture: progress comes from ordered
knowledge (a lock-free fold, a machine that needs no coordinator), never from
restraining the other party. And Theognis' emblem of mētis, the polyp, is the
generic machine itself: "hold the temper of the much-twining polyp, who shows
himself to the eye such as the rock he clings to" (πουλύπου ὀργὴν ἴσχε
πολυπλόκου, ὃς ποτὶ πέτρῃ, τῇ προσομιλήσῃ, τοῖος ἰδεῖν ἐφάνη, Theognis
215-218): one `Ideal`, taking the nature of whatever `Gate` it clings to,
causal against `Causal`, scalar against `Fifo`, participatory against a
caller's rule.
deinotēs (δεινότης):: The formidable, effective skill: the raw capacity to bring
something off (Aristotle's neutral cleverness that becomes _phronesis_ once aimed
well; in myth, what makes Mētis the wiliest, cunning against a deceptive world).
Aristotle defines it as the capacity to act toward a proposed aim and reach
that aim. The capacity is praiseworthy when the aim is good and villainy
(πανουργία) when the aim is bad. Phronēsis requires this capacity but is not
identical to it (NE VI.12 1144a23-30). That Bekker page states the charter's gating rule
first: the crate ships the δύναμις (the machine, the observable frontier), the
caller brings the σκοπός (the aim), because capability without an aim is
cleverness pretending to be wisdom. The same chapter names the aim-setter from
its other end: virtue makes the mark right (ἡ μὲν γὰρ ἀρετὴ τὸν σκοπὸν ποιεῖ
ὀρθόν, 1144a7-9), the half `ethos`, the consumer that brings typed aims, builds
on; the seam between the two crates is, textually, the seam inside one chapter
(verified from both sides, S82). The founding myth states the same rule
from its other side: Zeus swallowed Mētis "that the goddess might counsel him
in both good and evil" (ἀγαθόν τε κακόν τε, Theogony 900). The capacity
counsels both ways, so it is carried inside a governing discipline rather
than let loose, which is why the truer myth is cunning against deception, not
a merge catalog.
In `metis` it names a chartered, caller-defined dimension for what concurrency
should _do_ at a genuinely concurrent frontier (keep siblings, pick a winner, fold
a join, or distrust a lying peer), the decision-layer mirror of the _kairotic_.
Design only, held for sign-off and gated on a concrete caller
(xref:prd/0008-metis-deinotes-concurrency-resolution.adoc[PRD 0008]).
tyche (τύχη):: Chance, fortune, the genuinely contingent. What _mētis_ is _for_: cunning
is the intelligence that masters a world not wholly determined. In `metis` it is the
residue the causal gate leaves, the mutually concurrent frontier where the outcome is
open and the _deinotēs_ acts. Named because it is the thing "causal" would efface (see
_antichain_ under distributed-systems vocabulary). Aristotle places it exactly:
tychē is an _incidental_ cause, αἰτία κατὰ συμβεβηκός, at work where lines of
causation cross without either producing the other (Physics II.4-5,
196b-197a). The concurrent frontier is that crossing: the causal record
supplies no edge between its members, so whatever order the tiebreak imposes
is incidental to causality, which is why the machine surfaces the frontier
read-only instead of effacing it.
== Time vocabulary
[horizontal]
chronos (χρόνος):: Quantitative, sequential, measured time. The physical-clock
reading. In `Kairos` this is the 64-bit `physical` field, conventionally
nanoseconds. Supplied by a `TimeSource`. Aristotle's definition is a logical
clock avant la lettre: time is "a number of change with respect to the before
and after" (ἀριθμὸς κινήσεως κατὰ τὸ πρότερον καὶ ὕστερον, Physics IV.11
219b1-2). An HLC is that definition implemented, a counter numbering events by
before-and-after, anchored to a physical reading.
kairos (καιρός):: Qualitative, opportune time; "the right or critical moment."
The name of the implemented module and of the timestamp type `Kairos`. A
`Kairos` value fuses chronos, logical causality, a qualitative tag, and a
spatial identity into one totally ordered 128-bit stamp. Four sources each
hold up one design decision. Pittacus' maxim καιρὸν γνῶθι, "know the kairos"
(Diogenes Laertius 1.79), is a second-person imperative: only the caller can
know which kind of moment this is, which is why the kairotic is a
caller-supplied parameter (`ToU16`), never a library judgment. Sophocles
makes kairos "the greatest overseer of every deed" (καιρὸς γάρ, ὅσπερ
ἀνδράσιν μέγιστος ἔργου παντός ἐστ᾽ ἐπιστάτης, Electra 75-76): every event
bears a stamp, and the overseer presides, which is why the tag out-ranks
station identity in the total order. Aristotle locates the good of the
category of time in the kairos (ἐν χρόνῳ καιρός, NE I.6 1096a26): kairos is
a value dimension of time, not a position in it, which is why the tag is
qualitative and rankable at all. And Pindar allots it "a brief measure" (ὁ
γὰρ καιρὸς πρὸς ἀνθρώπων βραχὺ μέτρον ἔχει, Pythian 4.286): a qualitative
dimension must stay small or it swallows the order, which is why the tag
gets sixteen bits of the hundred twenty-eight.
kairotic:: A caller-defined `u16` tag embedded in every `Kairos`, marking the
qualitative kind or phase of a moment (for example: epoch, priority class,
workflow stage). It participates in the total order, ranking below logical
causality and above station identity. Supplied through the `ToU16` trait.
kairotic scheme:: A caller's protocol for interpreting the `u16` rank space:
which values are admitted, what they mean, their order, any constant-tag
opt-out, and how unknown values fail. Minerva supplies the field and its place
in `Kairos::Ord`; it does not register schemes or assign meanings. Equal tags
express no qualitative distinction and fall through to `station_id` when the
physical and logical fields also tie, so a collision is either deliberate
equivalence or caller ambiguity, never uniqueness. `0` is the conventional
neutral opt-out, not a wire-level reserved value. Stokes is the first
implemented admission-side scheme (S239): its `CommandClass` maps `1..=4` to
SafetyStop, Irreversible, Config, and Advisory, lower first; refuses `0` and
unknown values at ingress; and validates the typed class against the stamp.
The tag remains an equal-HLC tiebreak, not global priority or authority. Its
nonzero mints are still test-only, so the field-emission watch remains open.
logical:: The 16-bit Lamport-style counter that breaks ties when two events
share a physical reading, preserving causal order without requiring clock
agreement.
== Distributed-systems vocabulary
[horizontal]
HLC:: Hybrid Logical Clock. A clock that combines a physical reading with a
logical counter so that timestamps stay close to wall time while still
guaranteeing that causally related events are ordered correctly. Minerva's
`Clock` is an HLC extended with the kairotic field. It exposes the three HLC
operations as one fold: the *send* step (`now`), a *fused receive-and-send*
(`after`), and the pure *receive* step (`observe`, which advances past a remote
stamp without minting one).
station:: A node or clock instance, identified by a `u32`. In `Kairos`,
`Clock::new` requires a nonzero `station_id`. The identifier is the spatial
stamp dimension and the final total-order tiebreaker. The broader `metis`
station domain permits zero. A consumer can enforce a narrower identity
policy at its authenticated boundary. The caller must keep station
identifiers unique among participants. See
xref:prd/0001-kairos-hybrid-logical-clock.adoc[PRD 0001].
causal vs concurrent:: Two events are _causally related_ if one could have
influenced the other; they are _concurrent_ if neither could. Minerva imposes
a _total_ order over a partial causal reality: every pair of stamps compares,
but only the `after` relation carries a causality guarantee. The partition is
older than the vector clock: Aristotle's Categories separates priority in time
(the first and commonest sense of πρότερον, 14a26) from priority _by nature_,
where "that which is in any way the cause of the other's being is prior"
(14b11-13), and sets beside them things _simultaneous by nature_, where
neither is cause of the other (14b24 ff.). A `Kairos` scalar retains only the
first sense; the `VersionVector` recovers the causal sense and, with it, the
honest ἅμα, concurrency.
antichain:: A set of pairwise-incomparable elements of a partial order. In `metis` the
_ready antichain_ is the set of events deliverable at once *under the `Causal` gate* (and,
per source, `Fifo`): the *cover* of the delivered ideal (its minimal not-yet-delivered
elements, the outgoing cover edges from the delivered vector `D`), and a true antichain of
the event order in any duplicate-free valid history. Generically `Ideal::frontier` returns
the gate's _enabled set_, which is an antichain only for gates whose deliverability is a
cover over an event order (a threshold gate's enabled set is not; see
xref:metis-production-recording-decision.adoc[the production-recording-decision note]).
`D` is a _point_ in the lattice of consistent cuts (Mattern's lattice of global states),
and `merge` is the join it inherits; the antichain is the leading edge out of that point,
not the ideal's trailing _generating_ antichain `max(I)`. It is where causal order runs out
and the _tyche_ begins; `Ideal::frontier` surfaces it read-only so a caller can resolve a
genuinely open frontier (the _deinotēs_ dimension) rather than take the buffer's default
`Kairos`-minimal linearization. Grounded in xref:cut-lattice-and-frontier.adoc[the
cut-lattice note].
order ideal (down-set):: A down-closed subset of a partial order: if it contains an element
it contains everything below. In `metis` the set of _delivered_ events is an order ideal of
happens-before, the object the `Ideal` holds and advances (the lattice sense of "ideal", not
a directed ideal). By Birkhoff representation it is the same object as the delivered vector
`D`. See xref:cut-lattice-and-frontier.adoc[the cut-lattice note].
cover:: The minimal elements of an ideal's complement: what `Ideal::frontier` returns, the
leading edge whose release would extend the down-set. Distinct from the ideal's _generating_
antichain (its maximal elements, the trailing edge), which `metis` never materializes.
cut lattice:: Mattern's lattice of consistent global cuts. A delivered vector `D` is a _point_
in it; `merge` is the join, and `meet` (S78) the greatest lower bound, whose n-ary form over a
declared roster is the stability watermark. Finite runs are governed by Birkhoff representation (down-sets of
the event poset are points of the cut lattice); Priestley and Stone duality apply only to the
infinite-history limit, where a never-completing cut is the lone point at infinity.
Ideal (the delivery buffer):: The delivery buffer type: an `Ideal<T, G: Gate>` that
accepts `Event`s in any order and releases each only once its gate reports it
*stable*, never before its dependencies (S14b, renamed from `CausalBuffer` in S26,
generic over the gate since S27b;
xref:prd/0005-metis-causal-order-buffer.adoc[PRD 0005],
xref:prd/0009-metis-ideal-gate-generic.adoc[PRD 0009]). The name is the invariant it
maintains: under the `Causal` gate its delivered set is an *order ideal* (a
down-set, above) of happens-before, and each release grows the down-set by one. The
machine is fixed and the gate varies (`CausalIdeal`, `FifoIdeal`); the
`Kairos`-minimal linearization of the frontier belongs to the machine, so it is
identical under every gate (PRD 0005 R4). It carries the seam where the total
stamp order and the partial stability order interlock: `frontier` surfaces the
ready set read-only, `pop_ready` releases, and delivery (the ordered once-only
release) is deliberately distinct from a `Producer`'s receipt-level `observe`.
Producer (the send half):: The sender-side event producer, the *send* half of causal
broadcast whose receive half is the `Ideal`'s holdback-and-release (S15b,
xref:prd/0006-metis-event-producer.adoc[PRD 0006]). A `Producer<C = DynClock>` owns
one station's send-side causal state and mints `Event`s by the
Birman-Schiper-Stephenson send step: `produce` self-counts the event, snapshots
observed knowledge as its `deps`, and stamps it with `Clock::now`. `observe` is
the dual receive fold (knowledge merges by join, the clock advances by the HLC
receive rule), `try_observe` its bounded, trust-aware form (S73). It names an
*invariant*: one station runs one producer, because two producers over one clock
would each self-count independently and mint colliding dots. The `C` carrier
(owned `Clock<TS>`, `Arc<Clock<TS>>`, or `&Clock<TS>`, S73/S291) is a sealed
capability that abstracts only how the station's single
clock is held; it composes with an `Ideal` rather than owning one, since
receipt-level knowledge folds order-independently. Named by the agent-noun rule
its write-side peer copies (`Producer` is to `produce` as `Composer` is to
`compose`).
dot:: One event's identity in counter space: the pair `(station_id, k)`, the `k`-th event
from that station, `k >= 1`. A producer-minted event's own dot is `deps.get(sender)`
(the `Causal` gate's contiguity condition is exactly "the very next dot"), and `0` is
not a dot (the un-minted state; the gate calls a self-dot of `0` malformed). A
`VersionVector` summarizes a *gap-free* set of dots (a cut: everything up to `get(s)`,
per station); the exact have-set records an *arbitrary* set of them. A 0-based consumer
index maps `dot = sequence + 1` (the `pinax` interlock rule). Since S345 the identity
is a nominal type: `Dot { station: u32, counter: NonZeroU64 }` carries the non-dot-zero
law itself (ruling R-91), ordering exactly as the tuple it replaced; station validity
stays the consumer's authenticated-boundary law.
RawDot (the raw coordinate):: The zero-capable sibling of `Dot` (S345, ruling R-91): a
coordinate as a payload spells it, a movement target, a locus anchor, a label,
which may name the non-dot counter zero or a dot no store holds. Reads over raw
coordinates are total (the S117 dangling-anchor law); `Dot::try_from` is the one
crossing into identity.
have-set (exact):: The set of dots a replica actually holds, however disordered the
arrival: an arbitrary subset of the dot space, which no single cut can represent.
Shipped as `DotSet` (S83, xref:prd/0012-metis-dot-set-exact-have-set.adoc[PRD 0012]),
bracketed by two cuts: `floor()`, the greatest gap-free prefix it contains (its
*interior*, a genuine cut by construction, hence the honest `Stability` report), and
`high_water()`, the per-station maximum (the cover of its *down-closure*, a liveness
bound that over holes is only an upper bound of a cut, so never a stability report);
`holes()` names the difference, the repair read. The floor is only *lax* under union
while the high water is a join homomorphism (see the cut-lattice note's have-set
section), which is why replicas exchanging have-sets converge faster than replicas
exchanging floors.
base change (restriction):: Reading a family over the station base as far as a
sub-roster is concerned: every `metis` lattice object is per-station data (a
dot _is_ `(station, dot)`), and `restrict` (S89,
xref:prd/0013-metis-relative-base-change.adoc[PRD 0013]) pulls it back along
a sub-roster inclusion. Exact against every shipped fold and read because
the base is discrete (restriction selects whole fibers and never enters
one; contrast the floor's *lax* law under union, which crosses a fiber's
interior). Its verdicts carry a *one-way witness*: order is preserved but
not reflected, concurrency reflected but not preserved, so a concurrency
verdict on restrictions is global evidence while an order verdict certifies
nothing beyond the sub-roster (the *created-order hazard*: restricting,
comparing, and acting globally fabricates a happens-before out of
forgetting).
Scope (the restriction brand):: A restriction scope: an invariant lifetime brand
tied to one act of restriction, inside which restricted evidence may be compared
and outside of which the comparison does not typecheck (S109,
xref:prd/0013-metis-relative-base-change.adoc[PRD 0013]). It is the type-level
form of *base change*'s created-order hazard (above): restriction preserves
order but does not reflect it, so an order verdict on restrictions is order
*over the sub-roster*, never order tout court. `with_scope` mints a fresh
invariant `'brand`; `Scope::restrict` yields a `Scoped<'brand, T>` carrying it,
so two values born under different scopes never unify, and the brand certifies
the *invocation*, not the roster value (two scopes over equal member sets still
do not unify). `Scoped` deliberately has no `PartialOrd` (order is method-only
and branded); the one verdict that lawfully travels is concurrency (it reflects
globally, so it returns unbranded), and the named escape is `forget`, so the
diff says what it does.
descent (the exact glue):: Recovering one section from partial views, exactly:
`try_glue` (S89, xref:prd/0013-metis-relative-base-change.adoc[PRD 0013])
checks agreement on a caller-declared overlap (which stations *both* views
claim authority over, a deployment fact like the roster) and returns the
`merge`, refusing disagreement with a typed `Disagreement` witness. The
split it enforces: `merge` is the fold for *knowledge* (the larger count is
the newer fact), the glue is the fold for *authority* (two views claiming
one station must agree, or the disagreement surfaces instead of being
absorbed into a section nobody vouched for, the PRD 0011 R8 over-claim made
refusable). Sections cut from one vector always re-glue to it: the sheaf
condition, in code.
difference (the owed set):: The third connective of the anti-entropy triad, beside
the join (what we jointly know) and the meet (what we agree on): "what do I owe
you." `VersionVector::difference` (S95,
xref:prd/0014-metis-difference-reads.adoc[PRD 0014]) is the vector lattice's
co-Heyting residual, the *least* vector whose `merge` into the other side covers
this one ("the least gossip that makes you cover me"), specified by universal
property in xref:metis-adjoint-ledger.adoc[the adjoint ledger] before it was
built; `DotSet::difference` enumerates the exact owed dots (the serve list, the
dual of `holes()`'s fetch list). The load-bearing shape rule: the residual
carries the *claim to be reached* at each station where the debtor leads, never
the subtracted count, because the owed events are the spans `(b(s), a(s)]` and a
subtracted counter names the wrong dots. Batching, transport, and scheduling of
the repayment are the caller's.
causal pair (dotted store):: The production-side dotted object (S96,
xref:prd/0015-metis-causal-store-algebra.adoc[PRD 0015]): `Dotted<S>`, a
*dot store* (content tagged by the dots that minted it, the open `DotStore`
axis) bracketed by the *causal context* (a `DotSet` of every dot ever seen,
survivors and superseded alike, which never forgets). The asymmetry is the
mechanism: a dot in a context but not its store was *seen and dropped*, so
the pair's merge (the *survivor law*: a dot survives iff both stores hold
it, or one holds it and the other context never saw it) honors removals
without tombstones, cannot resurrect removed state through a stale peer,
and lets an unseen concurrent write survive a concurrent removal. State and
delta are one type and the merge is the only write; dot assignment
(`next_dot`) reads the context, never the store, because a store forgets
removals and would re-issue a superseded dot (the *doomed dot*). Payloads,
named CRDTs, and add/remove-wins are the caller's side of the axis,
permanently (ruling R-12's boundary); the sequence *structure* itself ships
in-tree as `Rhapsody` (below), a dot-shaped store like the others, the
boundary drawn at application semantics, not at composition.
DotStore (the open store axis):: The crate's second deliberately open axis (the
first is the gate, below): the trait a causal pair's typed half implements,
holding content addressed by dots (S96,
xref:prd/0015-metis-causal-store-algebra.adoc[PRD 0015]). It names the boundary
minerva draws at application semantics, not at composition: the dot-shaped
instances ship in-tree (`DotSet`, `DotMap`, `DotFun`, `Rhapsody`), and a
consumer whose store carries richer payloads implements the trait for its own
type, keeping every payload and every add/remove-wins choice on its own side
forever. The trait's laws are what make `Dotted::merge` converge: support
exactness, the *survivor law* (the one law distinguishing causal state from a
plain union), content follows the dot, the semilattice on covered pairs, and
fiber-wise restriction (PRD 0013 R2). Breaking a law breaks convergence two
layers up, so they are stated as contract, not description.
DotSet (the bare store):: The bare dot store: presence only, no content beyond
the dots themselves, the simplest `DotStore` (S83,
xref:prd/0012-metis-dot-set-exact-have-set.adoc[PRD 0012]). Its architecture is
that *one* lattice object plays *two* roles, the dotted-vector literature's own
economy: it is the *context* half of every causal pair (every dot ever seen)
and it is the exact *have-set* (above), bracketing an arbitrary subset of the
dot space by two cuts (`floor` the honest interior, `high_water` the liveness
horizon, `holes` the repair read between them). `merge` is set union, the join,
a pure fold-and-read material with no seriality hazard. The have-set *adoption*
stays held in reserve (ruling R-7, no field consumer receives out of order
today); the context role has been load-bearing in every causal pair since S96.
DotMap (the composition store):: The composition shape of the `DotStore` axis: a
caller-keyed map of nested stores, with the *pair's* one context vouching for
every level at once (S96,
xref:prd/0015-metis-causal-store-algebra.adoc[PRD 0015]). It names how the axis
composes without leaking the context downward: `DotMap<K, DotSet>` is an
observed-remove set keyed by `K`, `DotMap<K, DotMap<..>>` nests, and a caller
store slots in as the leaf wherever application content lives; `K` is the
caller's type and minerva never reads it. Its load-bearing invariant is
*canonical form*: a key whose store is bottom is absent, so "key present" and
"some dot survives under the key" are one fact, and a key vanishes from the
merge exactly when every dot under it is superseded. Disjointness is enforced
at insertion (a dot names one write, so it cannot straddle two keys; the batch
build `from_disjoint` refuses with a `DotCollision` witness).
DotFun (the payload store):: The payload store: per dot, the value that write
carried, the one value-carrying `DotStore` minerva ships in-tree, the
multi-value-register shape of the delta-CRDT literature (S102,
xref:prd/0015-metis-causal-store-algebra.adoc[PRD 0015]). A register is a
`Dotted<DotFun<V>>` (concurrent writes read as sibling dots for the caller to
rank), a keyed register map a `Dotted<DotMap<K, DotFun<V>>>`. It names the
axis's content-follows-the-dot discipline at its sharpest: *keep-self, equal by
basis*. On the honest basis a dot names one write, so a dot carried by two
stores carries one value and the merge keeps self's, needing no `V: Eq` bound;
a same-dot disagreement is a reused-station-id basis violation the clock
already trusts away, deliberately not policed here (policing would need either
a silent pick that hides corruption or a panic that turns a peer's Byzantine
act into a local crash).
Composer (the causal-pair write facade):: The write-side facade over one causal
pair (S121, renamed from `Scribe`): a `Composer<S>` holds a station identity
and a running `Dotted<S>`, and `compose` performs the whole write in one call,
assign the next dot, assemble a covered delta, merge it into the held state,
hand it back to ship, so the two sequencing disciplines a hand-roller can
forget (merge before the next dot; a delta must cover its store) become
*structural*, unbuildable through the facade. Generic over the open `DotStore`
axis (`Composer<Rhapsody>` writes a sequence, `Composer<DotFun<V>>` a
register); the causal-pair analogue of the event-side `Producer`, named by the
same rule as its peer, the agent-noun of its verb (`Composer` is to `compose`
as `Producer` is to `produce`). Mechanism, never policy: which dots a write
supersedes is the caller's semantics.
Rhapsody (the sequence store):: The sequence instance of the causal-store axis
(S101, renamed from `Weft` in S120;
xref:prd/0017-metis-rhapsody-sequence-store.adoc[PRD 0017]): a `DotStore` whose
content is a collaboratively-edited ordered sequence. An element's identity is
a dot and its place is a `Locus` (below); the grow-only ordering *skeleton* (a
`Locus` per dot ever woven) outlives the visible set, so a deleted element
becomes an *order tombstone* and its followers keep their place, and `order()`
reads a document order by an iterative skeleton walk. The name is a contract,
not an ornament (the peristyle criterion): a _rhapsōidos_ stitched epic verses
into one ordered recitation (_rhaptein_, "to stitch", + _ōidē_, "song"), which
is the mechanism exactly, an ordered whole *stitched* from concurrently
inserted fragments by the anchor-and-rank assembly, where the provisional
`Weft` named only the woven cloth. Ships the ordering structure; text,
payloads, cursors, and undo stay the caller's (PRD 0017 R10), and since S127
the interleaving cure is structural rather than the caller's problem (the
sided anchor, xref:prd/0018-metis-rhapsody-sided-anchor.adoc[PRD 0018]).
Locus (the placement):: Where an element sits in a `Rhapsody`'s order (S119,
renamed from `Thread`): `Locus { anchor, rank }`, the `Anchor` it hangs on
(`Origin`, or `After` / `Before` a dot, the sided algebra of
xref:prd/0018-metis-rhapsody-sided-anchor.adoc[PRD 0018], S127) and the
`Kairos` that ranks it among the siblings sharing that anchor and side (rank
*descending* in the bucket, the RGA rule, newest nearest the anchor on either
shoulder). The skeleton is a `Locus` per dot ever woven; a deleted element
keeps its locus as an order tombstone. The name is exact: in genetics a
_locus_ is a fixed position along an ordered sequence (a chromosome), which is
precisely a dot's place along the rhapsody. Renamed from `Thread` because that
word collides head-on with `std::thread::Thread`, a defect, not taste.
Scholia (the mark store):: The annotation instance of the causal-store axis
(S195, xref:prd/0021-metis-scholia-mark-store.adoc[PRD 0021]): dot-tagged
spans over a sequence's identity space, each a `Scholion { start, end,
tag }` whose ends are `Verge`s (sided identity boundaries: `Origin`,
`Before` / `After` a dot, `Terminus`) and whose tag is caller-opaque
forever. The projection onto the current order is the sequence's own read
(`Rhapsody::extent`), whose verdicts are total: covered (emptiness
honest), inverted, dangling, all surfaced and none repaired. The name is
a contract, not an ornament (the peristyle criterion): _scholia_ are the
marginal annotations keyed to spans of a classical text, living beside
the text without altering it, their interpretive content held in the
commentary rather than the text, which is the division of labor exactly:
where a mark sits and what the caller inscribed are the store's; what a
tag *means*, what nests, and how anything renders are never minerva's
(ruling R-23's mechanics-versus-meaning redraw).
Metatheses (the move record):: The movement instance of the causal-store axis
(S196, xref:prd/0022-metis-metathesis-move-machine.adoc[PRD 0022]): dot-tagged
placement testimonies, each a `Metathesis { target, to }` re-placing an
existing element (`target`, a dot whose identity never changes) at a new
`Locus`. Structurally the payload store applied to movement
(`DotFun<Metathesis>`), pure delegation, so it adds no merge semantics of its
own: concurrent moves of one element survive as sibling testimonies and are
resolved only in the `Recension` read (below), by the fixed public rank order.
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
movement preserves the identity a delete-plus-reinsert would fork, and undoing
a move is an observed-remove of its testimony. The name is a contract, not an
ornament (the peristyle criterion): _metathesis_ is the classical grammarians'
own term for transposition, the reordering of elements within a text
(_meta-_, "across", + _thesis_, "placement"), which is the mechanism exactly,
a re-placement of an element already in the sequence.
Recension (the movement replay):: The decision-layer read that resolves a
`Rhapsody` under a `Metatheses` record (S196,
xref:prd/0022-metis-metathesis-move-machine.adoc[PRD 0022]):
`Rhapsody::recension` applies the skeleton's births first (canonical, never
refused, since the weave skeleton is a forest), then the record's moves in
rank order (ties broken by the metathesis dot), refusing exactly the moves
whose application would place their target inside its own anchor cycle (so a
cycle is always broken by refusing the move, never a birth). It is a *sealed view*: it exposes the sequence reads by
delegation (`order`, the lazy walks, `extent`, placement and visibility) plus
the two surfaced verdicts (`refused`, `pending`), and deliberately no path
back to a mergeable store and no recording-possession witness, so the chosen
reading can never masquerade as the record (the production-recording-decision
rule, by construction). Since S203 (ruling R-30) the view is also
*maintainable*: `Recension::collate` brings it to the pair's current state
at the cost of the changed regions' replay work plus per-call possession
scans (since S205, ruling R-32: one `O(pages)` word-comparison walk over the visible occupancy planes plus flipped-dot extraction (the visible scan's cost no longer depends on its have-set fragmentation), beside the woven have-set diff (floor-compact on honest traffic) and the surviving-testimony record scan), the eager replay staying the contract form it must
agree with exactly. The name is a contract, not an ornament (the
peristyle criterion): a _recension_ is the critical text a philologist
derives from the transmitted witnesses, itself never a witness, which is the
type's discipline exactly, derived from the records and never folded back
into them; and to _collate_ is the philologist's own next act, re-reading
the witnesses against the derived text and correcting exactly where they
differ.
Since S226 (ruling R-44), a strictly forward local recipe may instead open a
`with_movement_batch`: intermediate placement decisions remain sequential in a
topology-only reading, while the positional thread is materialized once
before the closure owner returns. The scoped capability couples record and decision ownership and
withholds full order reads until the deferred coordinate is current again.
spectrum:: The dual space of the cut lattice: the prime filters of the down-set lattice `O(E)` under
the hull-kernel topology. By Stone duality it is a _spectral space_, and by Hochster's theorem
homeomorphic to `Spec R` for some (non-constructive, distributed-systems-meaningless) ring, which
is the precise sense in which the order theory resembles algebraic geometry. On a finite run the
spectrum recovers the event poset exactly but coarsely (a bare space, no structure sheaf); it is
the same Priestley dual the cut-lattice note scopes, re-presented through `Spec`. Chartered as a
held horizon in xref:prd/0010-metis-spectrum-algebraic-geometry-horizon.adoc[PRD 0010].
stability watermark:: The pointwise infimum `min_n D_n` of every node's delivered cut: what _every_
node has delivered, hence safe to forget (the matrix-clock garbage-collection line). It is the
_meet_ of cuts, a consistent cut and so a _point_ in the cut lattice (not a frontier), and the
algebraic-geometry reading is the gluing of the nodes' local sections into a global section.
Shipped in S78 as `VersionVector::meet` plus the roster-fixed `Stability` tracker
(xref:prd/0011-metis-causal-stability-watermark.adoc[PRD 0011]), the promotion of `VersionVector`
from join-semilattice to distributive lattice. The meet ranges over a *caller-declared* roster,
never "peers heard from so far" (an unreported member pins the watermark at bottom, and the empty
roster answers bottom, not the vacuous top); what is reclaimed below the watermark stays the
caller's policy. Its contract is Agathon's line (NE VI.2 1139b10-11, the revision boundary's
epigraph) read backward: only what is irrevocable everywhere may be forgotten anywhere.
Stability (the tracker):: The cross-node causal-stability tracker: the
roster-fixed object that folds each member's reported delivered cut by join and
reads their *stability watermark* (above) by meet (S78,
xref:prd/0011-metis-causal-stability-watermark.adoc[PRD 0011]). Where the
watermark is the *quantity*, `Stability` is the *object and its membership
law*: the roster is fixed at construction and off-roster reports are refused
(`UnknownStation`), because a meet is only as trustworthy as the family it
ranges over and the failure direction (forgetting below a wrongly high
watermark) is unrecoverable. `report` takes a bare vector, an R8 cut *claim*
the tracker cannot verify, and clears the witnessed gate; `report_cut` carries
a `Cut` (below), so `watermark_cut` can hand the meet back witnessed (S114).
Mechanism only: what is reclaimed below the watermark is the caller's policy.
Purview (the gossip tracker):: The per-peer causal-context tracker: the
gossip-targeting dual of `Stability`, one carrier down (S105; the witness
ledger in xref:crdt-vision.adoc[the CRDT vision]). For each roster peer it
holds the `DotSet` this replica can vouch the peer has seen, and reads the
per-peer `owed` ("what do you provably lack") where `Stability` reads a meet.
The name marks the safety direction that is the whole story: each row is a
*lower* bound on what the peer holds, so `owed` over-ships (a harmless
liveness cost the merge absorbs) and never under-ships. The one hazard, an
over-claimed row silently stalling convergence, is constructional: `note`
takes a `Received` witness (below), not a bare `(peer, DotSet)`, so hoped-for
contexts and misattribution do not typecheck; the single audited escape is
`Received::trust`. Roster-fixed and bottom-defaulting exactly as `Stability`.
Received (the receive witness):: Evidence that a context was received from a
named peer: which peer it came from, and the `DotSet` that peer demonstrably
held, since a peer cannot ship what it has not seen (S112; the witness ledger
in xref:crdt-vision.adoc[the CRDT vision]). The receive-side twin of `Cut`
(below): a witness minted only where the proof exists, guarding a fold
(`Purview::note`) that would otherwise trust an unaudited claim. Both fields
are private and the only honest mint is `Composer::absorb`, which testifies to
the context of a delta the peer actually shipped, so over-claiming a context
and misattributing its sender are both unrepresentable. The one door out is
`trust`, named for the burden it carries.
Retirement (the removal tracker):: The cross-node retirement tracker: the
removal dual of `Stability`, tracking which removed dots each roster member
has *applied* rather than how far each has received (S115,
xref:prd/0017-metis-rhapsody-sequence-store.adoc[PRD 0017]). It names the
witness `condense` requires and mint evidence cannot supply: removal deltas
mint no dot, so "removed and applied everywhere" is not derivable from a `Cut`
or the stability watermark, which witness what was *seen*, not what was
*applied*; it is application evidence only the deployment can gather.
`acknowledge` folds each member's applied set by join; `retired` reads the
meet, the dots *all* members have acknowledged. Roster-fixed and unrecoverable
in the same direction as `Stability` (an over-claim strands a laggard's future
anchor forever), so off-roster acknowledgements are refused and the empty
roster answers bottom.
Retired (the condense witness):: The evidence a set of removed dots has been
applied at *every* roster member: the one claim `Rhapsody::condense` and
`Composer::condense` accept (S115; the witness ledger in
xref:crdt-vision.adoc[the CRDT vision]). The inner set is private, so a
`Retired` is built only by `Retirement::retired` (the honest meet) or the
audited `trust` escape; a bare have-set no longer condenses. The type is the
difference between "dots I removed locally" and "dots removed and applied
everywhere", and only the latter is safe to excise; its `trust` door is the
removal-side counterpart of `Scoped::forget` and `Cut::into_vector`, the name
the warning.
Cut (the witnessed cut):: A `VersionVector` witnessed *gap-free by
construction*: a genuine cut, carried in a type whose only constructors are
the provably gap-free reads (S108,
xref:prd/0011-metis-causal-stability-watermark.adoc[PRD 0011],
xref:prd/0012-metis-dot-set-exact-have-set.adoc[PRD 0012]). It closes the
boundary the *cut claim* (PRD 0011 R8) left open: an honest cut and an
over-claiming upper-bound-over-holes are the same bare `VersionVector`,
indistinguishable at every seam, and meeting upper bounds over-claims
stability in the unrecoverable direction. `Cut` is construction, not
assertion: no `From<VersionVector>`, no `Default`, no `Deref`, and no wire
path, so holding one *is* evidence of honest local construction (`bottom`,
`floor_of`, `delivered_by`, `common_of`, closed under `meet` / `merge` /
`restrict`). It witnesses the moment of construction only: its sources are
monotone, so it never becomes a lie, but it may become stale, and a decoded
vector stays a claim.
epoch (the re-foundation):: The bounded-resources boundary's last face
(xref:prd/0024-metis-epoch-refoundation.adoc[PRD 0024]): a witnessed-cut
sweep of identity-bearing metadata that `condense` structurally cannot
release, staged as the pure fold (`Rhapsody::refound`, stage one), the
rounds (`Epochs`: declaration, confirmation, adoption, seal over
`Stability`, stage two), the boundary (`EpochStratum` / `EpochShadow` /
`EpochGate`: one window of old-addressed traffic judged in the old
epoch's own topology, only the deterministic outcome crossing, stage
three), and the carry (the seal consignment below, stage four's
document-plane half; the consumer's external-reference half stays gated
on the first adopter). The new epoch is a new dot space; the sealed
join is the duplicate recognizer, retained for a caller-declared `k`
generations.
seal consignment:: What a sealed window leaves the next generation (S263,
ruling R-50; named the seal *bequest* until the S266 rename, decided by
the owner on register: Latin _consignare_, to mark under seal, so the
verb's own etymology encodes the door's precondition, the `SealedEpoch`
witness it demands): `EpochShadow::consign`, the witnessed door that consumes
the shadow under its `SealedEpoch` and derives the opening base pair as
a pure function of the final delta set and the frozen map. The final
reading is re-spelled whole (window births at their judged places,
moved images where the old replay put them, window-deleted images as
order tombstones), the movement record is reborn empty, both pairs
share one gap-free translated context, and the retired map rides along
as the consumer's translation seam. The door refuses rather than
trusts: a foreign seal, a missing sealed-join delivery, carried
post-seal traffic, and an unfoldable reading each hand the shadow back
typed. Only the outcome crosses: verbatim anchors and carried
testimonies both fail the exact law (the rank-contest falsifier and
the S213 flip, `src/metis/tests/epoch_shadow/`).
gate:: In `metis`, the rule the `Ideal` uses to decide when a buffered event is _stable_
(safe to release): the `Gate` trait (`deliverable` / `advance` / `stale`), the seam the fixed
buffer machine runs over. Two gates ship as _peers_, neither a default: `Causal` (the
`VersionVector` happens-before rule, aliased `CausalIdeal`) and `Fifo` (a scalar per-source
watermark, `Dep = u64`, aliased `FifoIdeal`). A participation gate (a quorum over distinct
contributors) is a non-causal alternative, kept caller-side (consumed as a fold). The gate must
be _monotone_: once stable, always stable. There are three primitive laws, `stale` is
_terminal_ (up-closed), `stale` is disjoint from `deliverable`, and the joint up-set of
`deliverable \|\| stale` is itself up-closed, which does *not* follow from the other two
(amended S337). The buffer's drop and reclaim paths depend on terminality (see
xref:metis-gate-stale-contract.adoc[the gate-stale-contract note]). Athenian
procedure already states the stale law: "the laws do not allow the same man
to be tried twice on the same matter" (Demosthenes, Against Leptines 20.147,
the rule Rome codified as _ne bis in idem_). An event the gate has
adjudicated is res judicata: `insert` refuses the re-trial, and terminality
is the promise that no decided matter reopens (the gate-stale-contract note
takes the rule as its epigraph). Implemented as a
caller-parameterized seam in
xref:prd/0009-metis-ideal-gate-generic.adoc[PRD 0009] (S27b); the gate sits _below_ the frontier,
the _deinotēs_ resolver _above_ it.
monotonic:: A clock is monotonic if successive stamps from it never decrease.
Minerva's `Clock` is strictly monotonic per instance.
skew:: The gap between a physical reading and the clock's internal physical
component. _Forward skew_ means the stamp ran ahead of wall time (a remote
event pulled it forward); _backward skew_ means wall time regressed below the
last reading. Tracked in `ClockStats`, never silently corrected.
== Terms of art used in these docs
[horizontal]
adjoint ledger:: The record (xref:metis-adjoint-ledger.adoc[its own note],
S90) of which shipped operations are adjoints of which, kept because
adjoints determine laws wholesale and predict them for operations that do
not exist yet (`high_water -| from_cut -| floor` is the model triple: the
S83 asymmetric pair is exactly left-adjoints-preserve-joins against
right-adjoints-preserve-meets). Two review disciplines follow: a proposed
read that is an adjoint of something shipped has its signature and laws
fixed before design starts, and every right adjoint over a possibly-empty
index carries the vacuous-top trap (the empty meet answers "everything"),
so its empty-family value must be stated or the surface is not done.
assurance ladder:: The crate's rungs of verification strength, each with its
own trigger discipline: property tests (sampled laws, always-on, since S7;
*shaped* generators where uniform sampling cannot reach the deep branches,
S86), fuzz targets (unbounded adversarial input, per untrusted parser, since
S16b; extended when a trust class escalates, ruling R-8), Kani proof
harnesses (total for the core invariant and wire laws, symbolic for the
clock fold, and only ever over *heap-free* state, the owner's scope
amendment; since S86), Miri (undefined-behavior and weak-memory checking
over the threaded tests), and Creusot as the chartered-but-unbuilt deductive
rung for heap-backed laws. What earns which rung is ruled, not vibes: ruling
R-9 in `owner-comments.adoc` names the classes, the exclusions, and the
tool-fit boundary (a bit-blasting solver cannot afford symbolic collection
structure). The rungs are complements, not upgrades; a proven law keeps its
sampled test as the always-on gate.
held in reserve:: A material shipped for the shape of the ecosystem's known
falsifiers rather than for a live call site, under the R-6 discretion test
with its counterweight recorded (ruling R-7 is the model instance:
`DotSet`, whose consumers' cuts are all gap-free today). Reserve status is
honest only while rare; the license is the test, not the beauty of the
object. Current instances: `DotSet` (PRD 0012), the `FifoIdeal` recipe for
`pinax`.
material:: A reusable building block, not a framework. Minerva provides
materials for causal concurrency; it does not own the application's control
flow.
mechanism / policy split:: The crate's division of labor at every boundary:
minerva ships the *mechanism* (a bound, a typed refusal, a computed quantity)
and the caller owns the *policy* (what to do when the bound is hit, whom to
trust, what to forget). Instances: `try_insert` / give-up policy (S30),
`try_observe` / trust policy (S41), `Stability::watermark` / reclamation and
membership policy (S78); even a participation gate stays caller-side (ruling
R-4). A mechanism is honest _ahead of_ a caller only where a crate-wide
capability boundary already owns the concern and the hand-rolled alternative
fails unrecoverably rather than merely redundantly (ruling R-6,
`owner-comments.adoc`).
resilience pattern:: The four-part shape every face of the bounded-resources
boundary ships in, and any future face must: an opt-in mechanism beside the
untouched infallible default, a typed refusal carrying what the caller needs
to act, caller-owned policy, and an observability read beside the bound.
Named in xref:target_arch/boundaries.adoc[the target architecture's boundaries].
seam:: A trait boundary that isolates an effect (time, backoff) so the core
logic stays deterministic and testable. `TimeSource` and `Backoff` are the
current seams.
slice:: A unit of work with one coherent reason for change. The planning
vocabulary used in
https://github.com/OwlRoute/minerva/blob/main/todos.adoc[todos.adoc]
(repository only).