= Horizons: where minerva grows, and how to decide
:toc: macro
:toclevels: 2
The forward companion to xref:target_arch/index.adoc[the target architecture]. That
document pins what must not change; this one maps where the crate can go, one
avenue at a time, each with its *firing signal* (what un-gates it), its *distance*
(how close the signal looks from here), and the *intuition* a future session
should inherit rather than re-derive. Rulings live in
https://github.com/OwlRoute/minerva/blob/main/owner-comments.adoc[`owner-comments.adoc`] and slices in
https://github.com/OwlRoute/minerva/blob/main/todos.adoc[`todos.adoc`]
(both repository only; not shipped in the crate archive); this document is
the map between them. It is a
map, not a promise: nothing here commits code, and every avenue defers to its
ruling.
Dates and distances were last re-walked whole on 2026-07-16 (S262) against
committed `polis` `be56866`, `stokes` `fe74a49`, `ethos` `562cb43`,
`pinax` / `plethos` `7c1da2f`, and `alma` `415067e5`. Dirty Polis data-plane
and Stokes lineage-runtime worktrees were inspected only as candidates, never
as landed contracts. Polis now has durable causal state and a mutually
authenticated TLS handshake around the possession protocol whose `DotSet` v1
pin S243 already records. Stokes now supplies the first external custom
`DotStore`: an indexed effect store whose in-place merge is checked against
Minerva's canonical `DotMap` semantics. That adoption confirms the open axis
and the narrow checked-rehydration and allocation-free reads added for it; it
requests no new trait or public law framework. At that recorded cut Stokes
still had no production event mint or `Stability` retention flow. The focused
2026-07-20 intake below supersedes the latter observation.
S263 (same day, ruling R-50) then built PRD 0024 stage four's
document-plane half, the seal consignment, and its landing re-drew this map's
epoch territory: the protocol now runs end to end on the two document
planes with no scoped-out traffic class, which converts several formerly
abstract avenues into concrete instruments with named signals. Axis 13
below is that territory, written while the intricacies were fresh so a
future session inherits the intuitions rather than re-deriving them.
A focused 2026-07-20 intake against committed Alma `d9dfe844` and Stokes
`bf3c9d4` updates one signal without claiming a whole-map re-walk. Alma now owns
a certified fixed view, durable gap-free floor reports, and the existing
reclamation/refoundation decision over Minerva's `Stability`. That is the
first-contact triple gate axis 4 required. Stokes independently persists
witnessed-cut convergence and durable terminal retirement over its membership
document. Neither consumer needed a tracker shape change. At that cut the
release, wrapper, scale, tag-emission, revision, base-map, and
structured-document signals remained on their recorded gates.
S327's focused follow-up advances only Alma's transport record. The durable
owner record at `f37c3245` pins epoch-ledger v1 as a local storage contract;
`806d4ecf` admits lifecycle kinds 8 and 9 to Session Hello v3's
authenticated tuple; and `49c11873` runs the first non-empty transported
window with all nine kinds. The worked boundary's five digest rows are now
pinned on both sides. S328 adds Alma `1454e905`: crash-only stays byte-stable,
while Byzantine Hello v4 binds the exact configuration and negotiates the
Alma-owned kind 10 attestation. This fires the registry pin, not a Minerva
mechanism or release. S329 records Alma `a813c4ee` and `9d035920`: every owner
write and restore now compares retained proof history with the rehydrated
ledger before replay or authority escape, including a falsified pending-seal
crash shape. S330 records Alma TRANSPORT-20/21 at `a6b9e29d` and `728aa945`:
`ALMAEW05` closes the durable checkpoint lifecycle over roster receipts, and a
fresh process consumes exact-owner recovery capabilities before ordinary
authenticated anti-entropy repairs both successor replicas. The completed
schedule changes no wire kind or Minerva surface. The release, scale,
tag-emission, revision, base-map, and structured-document signals remain
gated.
S332 walks the next commit on that line, Alma `1d845cf6` (2026-07-21), a
design-only rewrite of stage B5's availability plan. Ruling R-82 finds the
trust charter's B5 gate unfired, every named fact is caller-owned or
expressible from shipped reads, and returns one correction:
`Epochs::horizon` is a transport fact, not a retention window, and a
body-release policy that also trims lineage proofs buys its joiners a
bounded recognizer hole. Axis 6 and axis 13 carry the disposition; nothing
shipped.
toc::[]
== How to use this map: the intake discipline
Slices in this crate are not born from the backlog table. The record so far: S78
came off a held PRD when an owner directive supplied the sign-off it waited for;
S83 came off a *consumer's* PRD, which had quietly defined a new object with a
clean minerva half; S85 came from a consumer's shipped machine changing the trust
class of an already-shipped surface; S86 came from an owner directive plus
tooling that happened to be installed. None of the four was a row in
`todos.adoc`. The rows are real work, but they are the *known* gated work; the
map below exists because the productive events are usually between the repos.
After every consumer intake, ask three questions, in order:
. *Did a listed gate fire?* The backlog's own question. Check the row's signal
and the governing ruling before treating it as fired; most "fires" on close
reading are adjacent interest, not the named trigger.
. *Did the exchange define a new object with a clean minerva half?* (The S83
lesson.) A consumer PRD that writes "minerva owns the X type and lattice"
has done the boundary-drawing minerva cannot honestly do alone. Verify the
claim against their live source, then weigh it under the R-6 discretion test.
. *Did a shipped surface's trust class change?* (The S85 lesson.) Same bytes,
same API, heavier adversary. Nothing is asked for, but obligations escalate:
R-8 makes the response automatic (record the pin, coverage follows the
boundary, bumps become coordinated).
Two standing disciplines guard the answers. Every consumer claim is verified
against their live source, never a relay summary (the S38/S40 discipline; the
sibling repos sit beside this one on disk). And every mechanism shipped ahead of
a caller must pass the R-6 test *and* record its counterweight as honestly as
ruling R-7 did; if the counterweight paragraph does not write itself, the answer
is no. "Held in reserve" must stay rare, because the queue of obviously good
lattice math is infinite and the license is the test, not the beauty of the
object.
== Axis 1: the release, and the two compatibility regimes
*Signal: FIRED (S341, ruling R-88).* R-2's import-shaped ask arrived, and by
the alternate route the paragraph below had named rather than the predicted
one: polis's Helen-coordinated `RTC-M1/g1` returned `Blocked(Decision)`,
authorize publication of the reviewed Minerva 0.2.0 package, because a
fresh Halina checkout cannot resolve the `../minerva` sibling path. The
pinax driver crate still does not exist; the coordination runtime's
reproducibility gate got there first. R-88's dispositions split the cut by
regime; R-92 (S346, the owner's 2026-07-29 directive) re-merged it: the
0.2.0 cut is prepared from the `dev` tip and includes everything on it,
the `metis` layer, the `Dot` newtype under the R-91 domain, and the whole
xref:prd/0028-metis-recorded-membership.adoc[PRD 0028] recorded-membership
program as dormant sibling code beside live v1. Wire conservatism is
carried by the shipped dormancy guards (v1 bytes frozen, v1 readers refuse
v2 whole, the v1 snapshot codec fails closed), and activation remains the
joint registry act. Publication remains the owner's one explicit external
action, which nothing in this repository authorizes.
*Distance (historical).* The predicted route was `pinax`'s host-side driver
crate (the binding of its anti-entropy `Session` to a substrate), with the
ask arriving as a CI break or a workspace manifest revert. Stokes is also
path-pinned and records the reproducibility tradeoff. Polis independently
recorded the same tradeoff at `be56866`, and its "first clean build in an
environment that cannot provide that sibling" was named here as the concrete
alternate route, which is, through Halina, the route that fired.
*Cut decisions.* First-contact hardening is complete before the
cut: Polis S2 satisfied `DotSet` R7 and Alma's certified-view transport satisfied
`Stability` R7, both without changing their lattice surfaces. The cut therefore
carries no provisional-additive decision. It must still distinguish the
crate's *two compatibility regimes*: the API migrates under semver with the
consumer guide's migration table as the release notes, but the wire frames do
not migrate at all. A frame is byte-identity contract (signature preimages since
S81, a network protocol since S85, ruling R-8), so the release notes state which
frame versions are protocol-embedded and by whom, and a version number that
implied the frames moved would be worse than no release. Third, the assurance
story is now part of the surface: the ordering contract and both wire codecs are
machine-checked (S86, ruling R-9), which is exactly the sentence a fourth-party
evaluator of a clock library wants to read; say it plainly.
*Beyond 0.2.0.* Expect the cadence to stay ask-driven. The crate should never
accumulate unreleased surface so large that a cut becomes a project; if the gap
ever again spans five primitives, that is a smell the R-2 trigger has been read
too narrowly.
== Axis 2: completing the anti-entropy family
The lattice story is complete *at one replica*: what I hold exactly (`DotSet`),
the greatest cut I can honestly claim (`floor`), how far I have heard
(`high_water`), what I am missing (`holes`), and, for a roster, the greatest cut
all have passed (`Stability::watermark`). What remains is *between* replicas,
and each piece has a distinct signal:
The difference read ("what do I owe you"):: *Shipped (S95,
xref:prd/0014-metis-difference-reads.adoc[PRD 0014], ruling R-11):*
`VersionVector::difference` (the co-Heyting residual; the adjoint ledger's
residual section implemented and cited, its first prediction fired in code)
and `DotSet::difference` (the exact owed-dot enumeration, the `holes()`
shape). What remains on this row is *adoption*: the original signal (a
second consumer hand-rolling an owed-set computation) now fires first
contact and any bounded, batched, per-station, or span-shaped variant, not
existence. `pinax`'s cut-level `delta` stands as its own ranked discharge;
the dot-granular read its rustdoc calls "the deferred dotted-version-vector
refinement" now exists on minerva's side of the R9 division, waiting.
The pairwise machine stays consumer territory, proven by `pinax` building
theirs without asking.
Polis S2 (`45b17aa`) is the first direct fact-level use of
`DotSet::difference`: it caps the lazy enumeration by fact count and payload
bytes, then resolves each dot through its own fact store. Adoption is landed,
and its shape confirms the boundary: scheduling, payload lookup, and both
budgets are caller policy;
neither a bounded iterator nor a Minerva repair session follows from it.
The `DotSet` deferred halves (S84):: The wire frame and the per-station repair
reads *shipped* as xref:prd/0016-metis-have-set-wire-frame.adoc[PRD 0016] (S98):
a canonical run-length `to_bytes` / `from_bytes` / `from_prefix` frame
(union-then-interior gossip, the lax law's payoff) and `holes_for` /
`hole_count`, born as the sibling codec with its own version byte, fuzz target
(`have_set_from_bytes`), and shaped proptests in one slice exactly as rulings
R-8 and R-9 pre-committed. The last deferred half is the bounded-exceptions
insert. *Signal: a consumer that bounds reorder exposure, or one that gossips
have-sets and adopts the frame* (PRD 0012 R7, PRD 0016 open questions).
The bounded-reorder and repair-read signal fired through Polis S2. It derives
possession from the causal context, calls `holes_for` / `hole_count`, and
preflights station, exception, hole, and forward-gap limits on a cloned
candidate context before one causal-store merge. That clone is bounded by
the very limits it checks and preserves whole-batch atomicity. A measured
cost may justify a reusable merge-side mechanism later. A one-dot
`try_insert` would not guard the actual `Composer::absorb` path and
must not ship as false assurance. Polis S3 (`5d10141`) calls the canonical frame under
its validated exception ceiling; S242 exposes that ceiling as
`HaveSetDecodeBudget` with exact and prefix decode variants while preserving
the standalone input-length default. S243 records that Polis possession
protocol v1 pins the inner `DotSet` v1 bytes and adds Minerva-side property
and fuzz coverage for the exact-slice, explicit-budget seam.
Stokes uses `DotSet` as the support of value-carrying causal records, not as a
receipt have-set. Its bounded record-frame harness now uses the canonical
context frame under `HaveSetDecodeBudget`, and its indexed store walks the
gap-free floor plus sparse `exceptions()` to find only causally affected
effects. The frame remains test realism rather than production transport, and
this is not the whole-batch bounded-admission measurement S84 names.
The production-side DVV (the causal store algebra):: *Shipped (S96,
xref:prd/0015-metis-causal-store-algebra.adoc[PRD 0015], ruling R-12):* the
imagined-primitives family 1 fired on an owner directive naming a
prospective multiplayer-editor consumer, and the kernel landed as the sixth
primitive (`Dotted<S>` over the open `DotStore` axis, the survivor law,
context-based dot assignment, `DotSet::intersect` firing the ledger's
second prediction on the way). Stokes first adopted the in-tree
`DotMap<EffectId, DotFun<Standing>>` composition, then `0a14aae` supplied the
first external custom implementation of the axis: a `Store` with an exact
dot-to-effect inverse index and a delta-bounded `causal_merge_from` override.
Generated partition schedules compare it with the canonical `DotMap` result.
Polis independently
adopts `DotMap<ThreadId, DotFun<Fact>>` through `Composer`. Polis validates
same-dot disagreement before total merge, exactly honoring `DotFun`'s
equal-by-basis contract without making the lattice fallible. No new Minerva
object or value join appears. Alma already closed first contact through
`Composer<Rhapsody>`. Stokes's implementation needed allocation-free wire
lengths and sparse exception iteration, both already landed, but no trait
change. Its own canonical-store oracle is the correct application-side law
check; exporting Minerva's internal foreign-store harness remains separately
gated. What remains here is sibling display order:
concurrent survivors rank for display by `Kairos`, the tag is the
discriminator, and the first varying-tag consumer is the one to design it
with.
== Axis 3: the deinotēs dimension, selective release built
*Signal fired.* Stokes brought the ruled case: it must hold a ready irreversible
command while releasing an eligible concurrent command. S234 ships the narrow
`Ideal::pop_ready_event_where` mechanism.
*What remains.* General concurrency resolution stays caller-side. A future request
for keep-siblings, winner selection, or join folding must bring its own concrete
shape; selective release does not imply a `Resolver<T>` framework.
*Result.* Selection and release share one mutable borrow; no copied frontier or
generation token escapes. The predicate filters only `Gate::deliverable` events;
the ordered scan restarts after each policy call so readiness changes are observed,
and refusal advances nothing.
Stokes owns class precedence and all authority.
== Axis 4: membership stays a seam, permanently
*First `Stability` contact fired and closed (2026-07-20):* Alma's committed
fixed-view transport supplies all three parts of the gate. `ViewCertificate`
is the deployment-authorized finite roster; `FloorReport` carries a gap-free
`Cut` under a stable-before-emit persistence fence; and the existing COLLAB-18
epoch refoundation is the reclamation decision the meet licenses. One
`InstalledView` owns one `Stability` across every carrier for the document,
persists its caller-owned report table before publishing, rebuilds the tracker
through `report_cut`, and exposes `watermark_cut`. The existing surface needed
no change. In particular, Alma did not ask Minerva to own certificates,
incarnations, persistence, transport, roster replacement, or the re-found
decision. PRD 0011 R7 is satisfied.
*Standing intuition.* Minerva must never own a membership protocol, a join/leave
state machine, or a failure detector; ruling R-4 (participation gates stay
caller-side) is the same instinct one layer down. The roster is a constructor
argument, full stop. If a consumer ever asks for "dynamic
membership support", the honest answer is a new tracker constructed over the
new roster, plus documentation of the regress/unpin semantics, not an epoch
protocol in this crate.
Stokes independently confirms the boundary after Alma's first contact.
Committed `1b37f98` gives `LineageRuntime<Draining, A>` sole ownership of a
private `Stability` over its canonical membership document. Local reports are
derived from checkpointed record context; remote reports bounded-decode a
prefix-only have-set back into `Cut`; attributed rows persist before the
tracker is rebuilt, and `watermark_cut` can produce only the typed witnessed
proposal frontier. Committed `4615cdd` adds durable terminal retirement after
that convergence. Stokes retains credentials, codecs, persistence, retry,
retirement policy, and live transport authority. It also needed no Minerva
surface change.
Polis explicitly defers `Stability` until a deployment has a fixed roster, an
authenticated durable application-delivery cut, and a concrete retention
operation. Its current possession floor is repair state, not yet such a
reported milestone. S241 therefore records a well-drawn future first-contact
path without firing this axis or weakening the fixed-roster seam.
S265 records the virtual-synchrony intake
(`docs/lit-review/leaderless-unanimity-barriers-virtual-synchrony.adoc`,
local and untracked; R-35's addendum is the tracked record, including
the enumerated falsifier schedules) without firing anything: the brief
confirms freeze-and-substitute as the mid-window failure semantics the
one-window discipline already enforces, offers the seal a guarantee
class (a whole-roster safe-prefix barrier, whose mechanism-side half
the S264 no-seal-outruns pin proves in-tree), and supplies seven
falsifier schedules plus the joiner staging rule (observer, reporter,
full member at the next sealed boundary) for the day the membership
charter fires. Its citations are transcribed, not verified, so these
stand as the brief's reading until the charter pays the verification
debt. The boundary this axis draws is unchanged and gained its
sharpest formulation yet: the eviction decision is a seam of evidence
authority, never of transition semantics, so minerva verifies
testimony and refuses its absence while the caller owns who leaves,
who joins, and when.
*S336 and S339 fire the departure half without moving the seam.* R-84
shipped `Stability::abandon`, one verb narrowing the family a meet ranges
over; R-86 shipped the `Departure` round that makes the abandonment bound
agreed and enforced, so the epoch rounds may substitute it for a departed
member's testimony. Read against this axis, both are the intuition holding
rather than bending: no roster changes, no join/leave state machine, no
failure detector, and the eviction decision stays exactly the seam of
*evidence authority* the S265 formulation named. What minerva now owns is
the evidence object and its refusals; who leaves, when, and on what
suspicion remain the caller's, and there is deliberately no detector, so
eviction on suspicion is never disguised as proof. Arrival is the charter's
live item and is the half that genuinely means a new tracker over a new
roster, which this axis has said from the beginning.
*S340 designs arrival, and the axis reads the refusal and it read the
build.* R-87 settles the specification and declines to ship it: the last
requirement is a durable endorsement fence in the epoch machine, which is a
wire change, so arrival is a 0.2.0 item. What the axis predicted still held,
because the seam is *evidence authority*, what an arrival agrees is an
**instant** rather than a value, and the joiner's staging needs nothing new
at all, since at a re-foundation every member's slot is already bottom. What
the axis did *not* anticipate is the asymmetry that stopped it: a replica
which fails to apply a departure is merely behind, while one which fails to
apply an *arrival* diverges. Timing is not part of an evidence object, and
that is why this half needs durable state where the other did not. Two
results are kept: departure became irreversible at a *door* rather than by
argument, which forces incarnation instead of recommending it; and the
concord is the crate's first cross-member comparison of one member's claim
against another's, which locates where a fork detector would live.
*S341 charters the durable state's shape, and the seam survives one honest
amendment.* Ruling R-88 and
xref:prd/0028-metis-recorded-membership.adoc[PRD 0028]: the admission rides
the sealed record, so the endorsement fence is deleted rather than enforced,
both admit doors vanish, and the roster becomes a *per-generation* quantity
a retained lineage proves. *S342 (ruling R-89) closed the composition R-88
left open*, a departure attestation racing an admission-tagged window,
by moving the tag out of the substitutable slots entirely: the arrival
round lives in the machine, the winning declaration carries its completed
boundary, assent rides each member's adopt door, and the record carries
what the winner declared. Content agreed at a seal has exactly two lawful
carriers, a value the rounds force, or a value whose absence blocks,
and a joiner set, which no lattice folds, had only the second. The
mechanism slice is unbarred and began the same session. The amendment this axis owes on its own words:
"the roster is a constructor argument, full stop" becomes "the roster is a
caller decision the record carries", who joins, who leaves, and when to
propose either remain outside the crate exactly as before; what enters the
record is the carriage of the decision, so that its taking-effect is an
agreed instant rather than a per-replica race. The eviction seam's
formulation extends to arrival unchanged: minerva verifies the agreement
and refuses its absence; the caller owns the choice.
== Axis 5: the assurance ladder, extended without sprawl
The ladder as of S86: proptest (sampled laws, always-on; *shaped* generators
where uniform sampling cannot reach the deep branches) under fuzz (unbounded
adversarial input, on demand) under Kani proofs (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 in R-9) beside Miri (UB and weak-memory over
the threaded tests). Ruling R-9 fixes what earns which rung; the day-one find
(the uninitialized-arm fold bug) is the standing justification and the standing
temptation, and the parser-harness failure (symbolic `BTreeMap` structure
sinking three successively smaller shapes) is the standing tool-fit boundary.
*Where it honestly extends:*
. *Creusot, the chartered deductive rung (probed S94, deferred on a measured cost).*
First correction to the earlier charter, which grouped both parser laws as
map-touching: that holds for the *bit-blaster* (Kani constructs the built
`BTreeMap`, the S86 sink), but for a *deductive* prover only the accept-path
*bijection* needs a map model. Parser *totality* and *mid-parse canonical
rejection*, the security-relevant laws, run over the byte sequence and a scalar
`previous` accumulator with the `BTreeMap` an opaque write-only sink, so they
need no map model. A dedicated S94 probe (a throwaway scratchpad crate mirroring
`from_prefix`, `creusot-rustc` built from source, the why3 plus four-solver
stack resolving) established both sides. *Reachable:* the `thiserror` mask
translates (a `cfg(creusot)`-gated derive with a trusted `Display` stub
compiles past `DecodeError`), the `BTreeMap` is an opaque total sink, and the
prover discharged *11 of 12* totality verification conditions, the twelfth a
routine slice-bounds invariant. *Costly, and unforeseen here:* reaching even
that took four rewrites of the shipped parser into Creusot 0.12's supported
subset, two of them the tool creaking on ordinary Rust: `ChunksExact` has no
`IteratorSpec` (an index loop is forced), array-destructuring
`let [a, b, c, d] = arr` *ICEs* the translator (`Unsupported projection
ConstantIndex`, a genuine upstream bug), and a derived `PartialEq`/`Eq` pulls
a `DeepModel` obligation (the eq-derives gate off under `cfg(creusot)`). So the
true cost is not "specification support for the map type" but contorting an
idiomatic, tested parser for an immature verifier, the proof tail wagging the
production dog. *The shape if ever pursued:* never in place, but a pure codec
core written Creusot-friendly from the first line (index-based, a plain error
enum so nothing to mask, `Vec<(u32, u64)>` so no map model), proven on its own,
with the shipped `from_prefix` a thin adapter over it; one move that dissolves
the mask, the map model, and the contortion together, the modularity avenue the
crate already leans toward. *Revisit when* Creusot clears the array-pattern ICE
(or a later release does), or a session is green-lit for the pure-core refactor
on its own design merit. Until then, shaped proptests plus fuzz stay the honest
owners and R-9's parser prong stands. (`creusot-rustc` is now built and cached
at the external target dir, so a future probe starts warm.)
+
*Landed (S187, ruling R-18), by exactly the recorded route:* the green-lit
pure-core refactor. The have-set frame's decode core is a *dual-homed pure
core* (`src/metis/dot_set/wire/pure.rs`: subset-clean from the first line,
contracts under `cfg_attr(creusot, ...)`, stripped by every normal build;
the detached `proofs/` crate `#[path]`-includes the same file and proves
it), with the shipped `from_prefix` a thin fold over its validated flat
output. Proved under `#[check(terminates)]`: termination, panic-freedom,
and the acceptance shape, 21 goals in ~1.3 s cold. The S94 cost verdict
inverted: written *in* the subset, the same toolchain proves in seconds
with no contortion. The owed contracts and the machinery rules are in
ruling R-18 and `proofs/README.adoc`; the store-algebra fence below is
untouched, and the next candidates queue behind the scoping note's
`StationDots` spike.
. *The gate laws, S75 shipped in S238 after stokes fired it.* `check_gate_laws`
now checks caller-generated ascending progress pairs for terminal stale,
disjointness, advance monotonicity, and stable up-closure without choosing a
property engine. Its typed input failures protect S237's componentwise-order
lesson: descending and incomparable states are not silently treated as a
chain. The dynamic released-only rule remains a per-combinator proof because
black-box cases cannot observe component admission. No further proof or
harness slice is open on this axis.
. *`portable-atomic` under Kani.* The clock proofs run on the asm-free
fallback (`portable_atomic_no_asm`), sequentially equivalent for the fold.
If `portable-atomic` ever grows a `cfg(kani)` the way it supports Miri, drop
the flag the same day and re-verify.
. *CI, when there is CI.* The kani and miri legs are manual today, recorded in
the DOCS status table. If the repo ever grows CI (likely at or after the
0.2.0 cut), the proof suite belongs in it at whatever cadence solver time
permits; a proof that stops verifying is a finding, not an inconvenience,
and so is a proof that stops *terminating* in its accustomed time.
*Where it must not go:* proofs for the application machines (`Ideal`,
`Producer`, `Stability`, `DotSet`). R-9 records why; the short version is that
their laws are algebraic over unbounded structures, already model-tested, and a
harness would either restate the implementation or dwarf-test what proptest
already covers. The S86 lesson cuts the other way too: the found bug lived in
an *asymmetry between two arms of one match*, so when two branches implement one
law, prove the law, not the branches.
== Axis 6: the trust boundary, deepened
The receive story is field-settled (the guide's field recipe: authenticity,
register, bounded observe, capacity; two consumers converged on it
independently). What remains on this axis:
The knowledge join (recorded as guide hazard 5):: `Producer::observe` folds a
received event's `deps` into knowledge by an unbounded monotone join, and no
in-crate bound can exist (unlike the stamp, where a local reading gives the
skew bound its reference point, a dependency counter has no local ground
truth). The defense is structural, a composition discipline, not a
mechanism: on an untrusted mesh, feed the producer from the `Ideal`'s
releases rather than raw receipt. Do not accept a future ask for
`try_observe_deps(bound)`; the honest reply is the discipline, because any
numeric bound would be theater with a type signature.
The adversarial deinotēs:: PRD 0008's darkest reading (distrust a lying peer)
stays gated with the rest of the charter. The identity models now exist at
both consumers (Ed25519 keyed by `station_id`), so if this fires it fires as
caller policy over minerva's typed refusals, exactly like every other trust
decision so far.
Cut claims under Byzantine reporters:: PRD 0011 R8 records that `Stability`
cannot verify a report is a genuine cut; an authenticated-but-lying member
can over-claim and steer the watermark into unsafe reclamation. This is
membership-trust policy (axis 4), caller-side by nature. If a consumer ever
needs it, the material minerva could honestly add is an *evidence* read
(which member's report pins which station), which is `reports()` today;
point at it before building anything.
Stokes has since landed its checked-action and exhaustive recovery model, but
the trust boundary remains Stokes-owned. Commit evidence is durable data and
execution authority is an affine capability; recovery reconstructs neither a
Minerva release nor an execution permit. Its versioned record-frame harness
embeds canonical `VersionVector` and `DotSet` frames, but the codec is private
and exercised only by the bounded adversarial model. It is not yet a production
protocol pin under R-8. The frame's checked `EpochAddress` reconstruction
required the already landed `try_from_parts` boundary (`f340552`), not a new
epoch authority capability.
Polis S2 draws same-dot conflict checks above Minerva's total merge. Landed S3
(`5d10141`) adds authentication and embeds the canonical have-set frame under a
bounded authenticated envelope. S4 makes the exact context part of atomic
recovery, and committed S5 `be56866` drives the signed handshake over bounded
mutual TLS. These later layers preserve the same inner bytes and validated
decode budget. S243 already records the strongest relevant trust transition:
Polis possession protocol v1 pins `DotSet` v1 and coverage follows the composed
parser boundary. TLS does not create a second Minerva pin or reverse dependency.
The witness line, restated (S332, ruling R-82):: This axis deepens by adding
*reads and refusals* under heavier adversaries, never by branding facts the
crate cannot observe. Durability was the first refusal (R-51: no local ground
truth for a caller's fsync), and availability is the same refusal one promise
longer, whether a checkpoint body will still be served is a fact about
someone else's disk and network. Alma's B5 reached that boundary from its own
side and put the capability where it belongs, in the caller. *Intuition for
the next trust ask:* when a consumer wants a witness, first ask which machine
performs the fact. If the answer is not this one, the honest reply is the
reads that let the caller build its own capability, plus whatever determinism
guarantee makes the caller's evidence mean something,
xref:metis-checkpoint-availability.adoc[the availability note] is the worked
instance, and the μή carries the standing prohibition.
== Axis 7: scale, when it is measured
Every performance avenue is parked on a workload signal, and should stay parked:
the dependency index behind `Ideal`'s linear frontier scan (S19), varint or
delta compression of vector frames (a PRD 0007 alternative, deferred), the
`write_to` batching encode (PRD 0007 open question; `pinax`'s session is the
candidate caller but shipped on owned frames without asking). A materials crate
optimizing without a measured caller is inventing its own workload.
*Intuition for when one fires.* Ask for the measurement in the ask ("what did
you profile, on what volume"); land the mechanism behind the existing surface
(the index is invisible, `write_to` is additive); and if the answer is a new
wire shape, it is a sibling codec with its own version byte, never an in-place
evolution (axis 1's regime rule). The likeliest first firing is `write_to`,
because the session's per-frame allocation is the kind of cost a driver crate
notices in its first profile.
The current consumer work does not supply a new number. Stokes's 4,096-effect
regression proves delta-bounded work for its own custom store, not a Minerva
performance request. Polis still clones one policy-bounded candidate context
for atomic whole-batch admission and has recorded no profile showing that clone
dominates. S19, S84, and the encoding avenues remain gated.
*The roster-scale dimension has its survey (S286, ruling R-68).* The RQ4
brief sorted the stabilization-transport field (clock-based freshness
against pure-asynchrony exactness against approximate gossip), and its
certified silence is claimed by the relay under-claim lemma in the
boundary-schedule note's section 7: exact tree aggregation of floor
claims is *already caller transport policy* through the unchanged
tracker (a subtree meet re-enters as each covered member's sound
under-claim; exact on complete waves, one vector per edge). So when a
roster number finally bites, the first answer is a topology the caller
wires, not a mechanism this crate ships; the intuition to inherit is
that freshness statements stay structural (waves, not seconds), the
advertisement plane never compresses (the oath fence needs per-emitter
stamps), and the reclamation meet never scopes except by genuine
membership or retirement action. The gate itself is unchanged: a
measured roster ceiling in a consumer's own profile.
*The axis grew two watched arcs (S189)*, both in the crdt-vision's table
with their evidence: arc 10, the owed-delta read (fired and shipped, S191,
ruling R-21: the witnessed owed read, flat across sizes), and arc 11, the
substructure program (the two-plane layout; all five phases shipped:
S194 ruling R-22 and S199 ruling R-26, the interned then run-coalesced
identity plane, 80 B/char floored to 20.75 B/char exact at 65k chars;
S200 ruling R-27, the order thread, offset and reverse reads at
nanoseconds where each cost a whole `order()` pass; S201 ruling R-28,
the coalesced child plane, the ordering closed form 20.75 to 5 B/char
exact; S202 ruling R-29, the segmented endpoint plane, the region
state 60x down to one segment per run; the contested-bucket cure and
any caller-shaped annotation remain the program's watched
territory in the arc entry). The type rules
any layout shell must satisfy (logical equality, ascending enumeration,
wire byte identity, branded non-`Ord` handles, paged construction, the
agreement pin) are fixed once in
xref:metis-shell-discipline.adoc[the shell discipline note]; the deeper
algorithmic scoping lives in `docs/miscellany/` (local, untracked) and
promotes through the arcs' own slices.
== Axis 8: the kairotic tag's second act
*First implemented scheme; emission trigger still open.* Stokes is the first
consumer to implement a nonzero scheme at a production boundary. Its
`CommandClass` is a caller-owned
`#[repr(u16)]` rank space: `SafetyStop = 1`, `Irreversible = 2`, `Config = 3`,
and `Advisory = 4`, with lower tags sorting first when physical and logical time
tie. `ToU16` is derived from the same discriminant as the class order, incoming
tags outside `1..=4`, including the neutral opt-out `0`, are typed refusals, and
`EffectDelivery::try_insert` rejects a payload class that disagrees with its
stamp. Selective release then uses the class order explicitly for global backlog
policy because the stamp tag is only an equal-HLC tiebreak. This is an
admission-side scheme, not yet a field emission: nonzero tags ride real
`Kairos` events in the bounded-delivery tests, while production code validates
and orders caller-constructed events but owns no clock, producer, or mint path.
The earlier field postures remain valid beside it. `Pinax` deliberately emits
constant `0`; `ethos` threads a caller-supplied tag end to end but its current
faculty still supplies `0`. Those are constant-tag opt-outs, not evidence
against the field. Stokes sharpens but does not close the stamp-layout reopen
condition: the consumer-side scheme exists, and the remaining trigger is its
first non-test path minting or emitting one of those values. At `fe74a49` it has
a durable station claim, but the effect writer remains test-constructed and no
clock, producer, or event mint exists outside tests. The dirty lineage-runtime
candidate adds none of those minting capabilities. S239 records the resulting
tag-scheme vocabulary in the glossary and consumer guide. No Minerva code or
frame changes.
*Intuition.* A tag scheme is caller protocol: it defines the admitted rank
space, the meaning of equal tags, its neutral opt-out, and how unknown values
fail. Minerva provides only `u16`, `ToU16`, and the total-order position. The
tag never becomes authority or global priority: physical and logical time still
rank above it, and equal tags fall through to station identity. S86's found bug,
which inverted domination through this tiebreak, remains the assurance warning
for any future ordering change.
== Axis 9: sibling machines
Two chartered non-`Ideal` machines wait on callers: the retrodictive read (S33,
a never-stale gate plus `pop_ready_event`, for a caller that re-decides
downstream) and the Bayou-shaped tentative sibling (S36b, genuine revision with
tentative, finalized, and retracted states). The revision-boundary note holds
the line that matters: genuine revision cannot live in the holdback `Ideal`,
because monotone progress cannot un-pass a dependency. If a consumer arrives
wanting "undo", route them through that note first; most "undo" asks are
retrodictive reads (cheap, additive) rather than revision machines (a sibling
with retained history and different truth semantics).
Stokes has landed its durable journal contract, affine checked actions, and
bounded exhaustive recovery model. It still asks for no Minerva read: recovery
classifies Stokes-owned facts without reopening an `Ideal` release or
reconstructing authority. That stronger implementation confirms that the
journal is neither S33 nor S36b and fires neither.
== Axis 10: the relative base
The core shipped in S89 under ruling R-10
(xref:prd/0013-metis-relative-base-change.adoc[PRD 0013]): `restrict` on both
lattice types (base change along a sub-roster inclusion, exact against every
fold and read) and `try_glue` (exact descent with the `Disagreement` witness,
the authority fold beside the knowledge fold). What remains held there has two
distinct signals:
General base maps (PRD 0013 R6):: Pullback along a station map that renames
rather than merely includes. *Signal: a consumer bridging station-id
namespaces* (federating two deployments, an id-translation boundary).
Distance: no consumer has two station namespaces today; the likeliest
origin is a `pinax` deployment merging with another. Intuition: ship the
bijective rename first, as a read; a non-injective map duplicates testimony
and waits for its own ask.
The n-ary cover fold (PRD 0013 R7):: `try_glue` over a declared family of
sections. *Signal: partial-view gossip*, reports that genuinely cover
sub-rosters; the `pinax` driver's relay layer is the plausible first, the
same prospect as the knowledge matrix's (which would fire together with
this, and should be designed together if it does). Intuition: a fold over
the binary read, cover as constructor argument in the `Stability` mold.
Two standing composition notes, so they are not re-derived: the axis 2
difference read composes with restriction ("what do I owe you about the
stations you track"), *discharged in S95* (the commutation law is
property-tested on both carriers under PRD 0013 R2, the first shipped
composition of the two families); and axis 4's roster-change intuition gains
the honest bootstrap, restricting the surviving members' reports into a new
tracker. Alma's first contact confirms the new-tracker boundary; it does not
authorize in-place membership mutation.
== Axis 11: the structured document
Chartered whole in
xref:prd/0019-metis-structured-document-horizon.adoc[PRD 0019] (S184, owner
ruling R-16), the structured-data expansion: the `DotStore` axis closed
under kinds (the node coproduct), movement (the replay-read move machine),
and annotation (identity-anchored marks), with the block-document recipe
probe as the measurement instrument that fires the rest. The PRD owns the
stages, hazards, and signals; this axis exists so the intake checklist finds
them.
Stage A, the block-document probe:: *Taken* (S186,
`src/metis/tests/studio/blocks/`): the recipe carried the block editor's
happy path, the conjunction read classified every delivery interleaving
for non-empty traffic (the empty block is the recorded limit: absence
cannot say "empty"), and the kind conflict surfaced exactly as expected,
one notch sharper (a kind reassignment cannot be one covered delta
across parallel maps). The evidence is recorded in PRD 0019's stage A
section and read in ruling R-17.
Stage B, the node coproduct:: *Taken* (S190, ruling R-20,
xref:prd/0020-metis-node-kind-closure.adoc[PRD 0020], on the gate R-17
fired): the sparse-product `Node<K, V>` ships the composite kind law
(product-lawed merge, surfaced `kinds_present()` / checked `sole()`,
exclusivity as the one-covered-delta write discipline), with the axis
conformance run, both losing shapes' counterexamples, and the coproduct
dissolution as shaped tests; the closure argument is the
xref:metis-store-algebra.adoc[store-algebra note]'s. The wire frame
stays out (PRD 0020 R7 records the depth-budget duty for the day it is
asked for).
Stage C, the move machine:: *Reorder half taken* (S196, ruling R-24,
xref:prd/0022-metis-metathesis-move-machine.adoc[PRD 0022], on the
field-pinned identity fork alma COLLAB-8): movement ships as testimony,
`Metathesis` / `Metatheses` (the grow-only record in the monotone sea,
pure `DotFun` delegation), and `Rhapsody::recension` is the
decision-layer replay: births first (never refused), then moves in one
`Kairos` order, cycle-formers (only moves) refused deterministically and
surfaced, nothing detached.
Identity is preserved by construction, so the delete-plus-reinsert fork
is unbuildable through this path; undo is an observed-remove of the
testimony. The cost model is discharged by the `recension/{n}` sweep;
the R7 seam *fired* (S203, ruling R-30: `Recension::collate`, the
maintained view, costing the changed regions' replay 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,
beside the woven have-set diff and the surviving-testimony record
scan, with
the eager replay the contract oracle; the gate's adoption number was the deadlock, read as
R-21 read arc 10's; the same-day adoption profile priced the
fragmentation term, the consumer guide's record). *Still gated:* the
subtree-across-containers half (a block leaving one container's sequence
for another's), waiting on the structured surface, where cross-sequence
testimony lives being the open design; the axis-9 sibling machine is its
structural neighbor.
Stage D, the mark store:: *Taken* (S195, ruling R-23,
xref:prd/0021-metis-scholia-mark-store.adoc[PRD 0021], on alma
COLLAB-7's filed range ask): the `Verge` sided-boundary vocabulary, the
`Rhapsody::extent` projection with total verdicts (covered, empty,
inverted, dangling; tombstone boundaries still bound), and the
`Scholia` mark store (spans opaque-tagged under the survivor law, the
register recipes for sharing, `anchor_dots()` as the retention
interlock's read). Expansion is the side choice at mint, no behavior
field; the rich-text-schema refusal is redrawn by the ruling at
mechanics versus meaning. The stage C intersection (a mark across a
concurrent subtree move) is the recorded shared open question.
The S262 walk reaches Alma `415067e5`. Its collaboration-facing change publishes
the same revision-paired text delta after peer absorption that local edits
already publish; the shared-text, Rhapsody, cross-container subtree, and
mark/move contracts do not change. Stage C's remaining half and the shared
mark/move question stay gated.
== Axis 12: the kairos minting program
Chartered by ruling R-19 (S188), which also shipped the keystone: the clock
unfused into one proven pure fold (`clock/fold.rs`, the whole time algebra
as a heap-free `const fn`) under two commitment shells (`Clock`, the CAS
loop; `LocalClock`, the `Cell`: no fences, no retries, `!Sync` by
construction), shell agreement pinned by property and the S86 proofs
covering both by construction. The remaining program, each entry through
its own slice on its own signal:
The generic-source rework:: *Pre-staged for the open 0.2.0 release cut as S291.*
`Clock<TS>` and `LocalClock<TS>` preserve the owned source type;
`DynClock` and `DynLocalClock` are explicit erased aliases. `Producer`
accepts the sealed `ClockCarrier`, so concrete, borrowed, and shared clocks
keep one station identity without forced erasure. S22 is closed; the release
cut remains open on the separate `Dot` domain decision.
Batch mechanics:: *The reservation half FIRED and shipped* (S211, ruling
R-33, on S210's paste number): `now_run(len, kairotic)` on both shells,
one reading and one commitment reserving `len` consecutive send
positions, the fold generalized by the closed-form `rank_offset` proven
equal to the iterated send (three new Kani harnesses). This discharges
the chartered `reserve(n)` in its honest form (the reservation returns
stamps, not raw positions). `observe_join` (one committed receive of a
batch's join) still waits on its own signal: a bench number on contended
receive throughput or a consumer folding stamp batches.
`KairosRun`, columnar stamps:: The *reservation receipt* now exists as the
public in-memory type (S211: `KairosRun`, crate-private construction
from the minting shells, members derived by the shared successor rule,
consumed by `Rhapsody::weave_run`). What still waits is the *standalone
columnar codec* (a run-length wire frame for stamp columns as a value,
its own version byte): its signal stays a consumer asking for stamp
columns on the wire, the adoption re-point in the R-11 pattern. The
snapshot codec's rank column (S197, ruling R-25) remains the wire
precedent: fixed-width records, never varint rows; the same successor
rule serves wire, memory (crdt-vision arc 11's run-coalesced skeleton),
and the clock, one law in three homes and now a fourth (the
reservation).
`chronos` adapters (std):: a coarse cached time source above all (at bulk
rates the OS read dominates before the CAS). *Signal: a consumer
measuring mint cost on an OS-source hot path.*
Minor:: a `Reach` min/max stamp monoid (parallel-reduction staleness, a
future observability feeder); per-shard station-allocation recipes in
the consumer guide when a parallel consumer exists (allocation itself is
identity policy, never a mechanism).
*Boundaries (R-19, restated):* no async, no executor, no scheduling; no
`Kairos` layout or frame change (frozen in preimages, R-8); no vector time
in kairos; no wait-free claims.
== Axis 13: the epoch proving ground
The epoch program (PRD 0024) is protocol-complete on the document planes
since S263: fold, rounds, boundary, and carry, with the fleet driving
births, moves, and deletes across open windows under adversarial
schedules. What remains on this territory is not more mechanism; it is
proof that the mechanism keeps its promises under the conditions it was
built for, plus the one half that only a consumer can finish. Each avenue
below has a signal and an inherited intuition; they are ordered by how
much each one would grow the crate's honesty.
The closing measurement (longevity with retention on):: *Ran as S268
(ruling R-52); the curve flattens, and the thesis is proven by its own
instrument.* The whole charter fired on S210's curve: 56 live elements
ballooning to a 13.2 MB snapshot at one million events. The charter's
cost section claimed steady state becomes `O(live + one window's churn +
one shadow)`, and S268 observed it: the S210 fixed-live churn mix run as
two arms over one seed (`bench/src/bin/longevity_epochs.rs`, the
epochless control against a 20k-event declaration cadence driving the
full declare/confirm/adopt/seal cycle from shipped parts), the control
reaching 700,000 current-plane skeleton dots and a 13.66 MB snapshot at
one million events while the retention arm's current plane stays between
14,280 and 14,308 dots and about 279 to 286 KB across the 100k, 300k, and
1m checkpoints, testimonies at 783
against 39,983 (the
movement plane reborn empty every seal). Neither suspected residual
(testimony-anchor pins, the first epoch's whole-history shadow) resisted
the sweep. The Helen review corrected the evidence boundary before cut:
pre-consignment rows now account for the frozen plane, base, both logs,
the real shadow and its maintained decision surface, native view, causal
contexts, translation map, projection, and bounded lineage separately;
a second review completed the shadow evidence with every decision log,
guard, possession mark, and ancestry count/capacity;
the total text skeleton is 57,760 at seal one and cycles no higher than
58,952 thereafter. Every seal compares its complete witness across the
roster. The record is
https://github.com/OwlRoute/minerva/blob/main/bench/reports/2026-07-17-longevity-epochs-closing.adoc[the
closing report] (repository only), and the alma outreach's promised churn curve now
exists. What the measurement named instead: the per-boundary cost is
asymmetric, the seal fold history-flat (2.59 to 3.50 ms) and the
adoption-side stratum rebuild linear in the window's churn (0.71 to 2.70
s per 20k-event
window on the run machine), so cadence is the knob trading retained
bytes against boundary seconds. *S270 (ruling R-54) attributed and
mostly retired that term by the same instrument's phase split:* the
dominant cost was one maintained-surface collation per replayed window
delta (the whole declarer-position spread), cured by the shipped batch
doors and the fused `EpochStratum` (one recension serving fold, surface,
and projection, the pristine core retained); the remaining log re-merge
is scheduled in the recipe across the declare-to-adopt gap (a delivered
declaration pins its candidate's cut, the declarer's dry-run seeds its
own staging, and a winner-or-cut mismatch falls back to the full
rebuild), landing the boundary stall at 36.8 to 39.1 ms on the
uncontested rotation with every deterministic column unchanged. *Intuition for the next firing:* the
*continuously* maintained cut-state (advance a trailing pair as the
watermark rises, before any declaration) now carries a soundness gate
beside its consumer gate, owned since S270 by
xref:metis-boundary-schedule.adoc[the boundary-schedule note]: local
meets are incomparable across members (the lag lemma) and the
survivor-law merge cannot back up, so watermark-led advancement can
overshoot the declared cut unrecoverably. *S282 (ruling R-64) carried
the fourth of the note's soundness shapes to a conditional proof*:
the declaration oath (a member's advertised watermark binds its own
future declarations from below, the capability structure the RQ2
research brief found to be the literature's only sound frontier
form), generation-scoped after the review's first finding (the
reborn coordinate space reuses numerals, so the oath table resets
at seal and stale generations are excluded at the fold door), and
honest about its one unowned premise after the second: no existing
transport law grants cross-kind per-emitter delivery order, so the
own-station stamp fence is a chartered registry obligation, checked
rather than assumed, with the no-silent-overshoot law (detected
rebuild, never a wrong stratum) proven for broken order. The pins
are `src/metis/tests/boundary_schedule/` (directed door pins, the
generated lifecycle sweep, and eight deterministic model pins; all
eleven defenses mutation-verified, the fence's lawful-duplicate
absorption, the snapshot rule, the ceiling refusals, and both
restart rules included). The design gate is thereby reduced to a
checklist: the arc ships only for a consumer whose declare-to-adopt
gap is too short for the scheduled recipe to hide the fold (the
R-30 shape twice over), and with the joint registry acts the oath
needs, the advertisement event kind plus its pinned fence contract
(the frozen PRD 0025 table carries neither today). *S285 (ruling
R-66) absorbed the RQ3 brief as the oath's policy axis*: the roster
meet is the maximal chooser-agnostic bound (pinned at family
grade), the
per-emitter kernel makes a caller-scoped sub-roster meet safe
against exactly the members whose held oaths cover the base (the
coverage lifecycle invariant) with the uncovered miss the
base seam's
detected rebuild, the scope is R-4 caller data that never crosses
the wire (no new registry act), and the counterweight's
advertisement traffic re-prices scope-linear, a singleton scope on
the closing instrument's uncontested rotation; the straggler and
post-seal re-arm cliffs thereby become priced policy choices while
the consumer gate and both registry acts stand unchanged.
The crash-restart arm (the rehydration recipe):: *Built as S264 (ruling
R-51), fired on the durability-and-recovery intake beside the standing
discretionary signal; harness and recipe only, zero shipped mechanism,
so the closing measurement's ordering above is honored.* The prediction
held: `Replica::rehydrate` is a pure replay of a modeled durable store
(one checkpoint per seal plus fenced notes) through the ordinary
inbound door, the `Adopted` witness is re-earned by re-running `adopt`
exactly as this entry expected, and the kill-restart alphabet rides
the generated law. What the arm sharpened beyond the prediction: the
minimal durable set is the replica's *own testimony* (its mints, its
retirement oath, its round positions' bases, the seal checkpoint),
because the roster-meet gating turns every lost receipt into a
liveness wedge the repair lane cures; three falsifiers price the three
violations (identity fork, stranded oath weave, masked-report wedge),
and PRD 0011 R8 gained its second face (a report is a durability
claim). The recipe's tracked home is the fleet module note. What
deliberately did not ship, and should not without new ground: a
library `Durable` witness or incarnation tagging in `Stability`; no
local ground truth exists for a caller's fsync, so a shipped brand
would be the deps-bound `try_observe` theater the anti-avenues refuse,
and detection-after-the-fact adds nothing the meet gating does not
already fail closed on. Bayou's lesson stands, now with evidence on
this side of it.
The epoch schedule tape (fuzzing the protocol):: *Built in-tree as S289
(ruling R-71), on the standing discretionary license.* Bytes drive the
fleet scaffold-free (`src/metis/tests/fleet/tape.rs`): declarations
race undelivered traffic, severance accumulates, members crash between
rounds, and the closing heal-and-drain asserts the charter's
fleet-wide laws with deliberately no ambient repair, so repair-lane
holes surface instead of healing silently. The prediction that the
first crashes would be harness-adjacent held with interest: the tape's
first pinned catch falsified the restate lane's own assumption (a
member crashing after the fleet seals could never again pass its seal
gate, peers' live reports parking at the laggard), cured by re-stating
the sealed join as every member's proven floor under-claim (the S286
license applied to repair). The S288 stray closed with it: the
displaced-window corner is unreachable by construction under the
honest recipe (evidence-grade, with a loud tripwire, the detector
pinned on the S284 fixture). *The libFuzzer leg followed as S331
(ruling R-81), on R-71's own charter*, by exactly the reserved route:
the harness is *exposed*, not copied (`metis::fuzz_harness`, a
`cfg(fuzzing)` module cargo-fuzz turns on for the whole build and no
Cargo feature can reach), so the coverage-guided driver runs the
shipped replica recipe rather than a fork of it. Its prerequisite came
with it, the one R-71's counterweight named: the fabric gained an
addressing door (`step_addressed`) and the tape is now read from both
ends, ops from the front and one delivery address per delivery from
the back, so transport order is *driven* rather than sampled while
every pinned seed keeps its byte-identical seeded schedule.
The addressed arm's
coverage is not a superset of the seeded arm's (the two consume the
tape differently, so neither corpus carries over), which is why the
displacement tripwire now sweeps both arms; and this is a
deliberate-run instrument rather than a cheap one, since an iteration
builds a fleet and runs whole lifecycles. *S347 (ruling R-93) took the
bootstrap-admission depth as a sibling tape*, preserving every epoch
corpus byte while adding partial arrivals, endorsements, joiner bootstrap,
and departure attestations over moving membership. The harness is still
exposed once rather than copied; both seeded and addressed arms have
always-on proptest twins. The remaining depth here is retirement
acknowledgements and condense, only when their schedule space earns the
cost.
The strong-list oracle:: *Built as S288 (ruling R-70), on the standing
discretionary license.* Attiya et al.'s strong-list specification
order core runs as an implementation-blind execution checker
(`src/metis/tests/strong_list/`): every visible order the convergence
tape twins observe enters an order ledger whose verdict is one witness
total order or a constraint cycle carrying its observations as
evidence; the parent-with-side to insert-at-position translation (the
lit-review's named first deliverable) is pinned at every tape weave;
and the cross-seal arms in `tests/refound.rs` compose the oracle with
the epoch boundary through the frozen rename map, the consignment's
opening-read pin at specification grade. Refusal capability is proven
by the oracle's own falsifier exhibits and four deterministic mutation
kills. Satisfaction is evidence-grade over sampled executions, not a
theorem; movement stays outside the specification by its own
semantics, and the FugueMax corner stays PRD 0018 R6's residual with
its scoping now executable.
The consumer half of stage four:: *Fired and field-consumed as S269
(ruling R-53), by alma COLLAB-17/18.* The adopter took the full boundary
through shipped public doors. Its 4,438 fertile tombstones fall to zero,
8,876 loci sweep across two replicas, and the late-joiner bootstrap resets
from 820,323 to 60,547 bytes over 1,440 live characters. Glyphs re-key,
cursor anchors translate or degrade to their unchanged order slot, marks
and byte-span undo cross no identity today, and the retired map's current
retention window is therefore zero. The consignment seam held at first
contact with no reshaping request. The one additive correction to the
charter's inventory is load-bearing: dotted deletes and a *single event
allocator* are paired conversions. Every adopted plane and protocol event
must draw from one event space per station, or independent plane-local
composers can mint colliding counters that the affine map cannot separate.
Alma uses the movement pair's context as that ledger; its union context is
gap-free and yields the honest `Cut::floor_of` report. `Composer` remains a
one-pair facade. A station-scoped ledger or reservation capability above
composers is a watched ergonomic shape, not a hidden allocator added to the
facade before a caller needs that migration. The next live question on this
entry is identity-anchored undo: generation-qualified records, translation
through a caller-declared map lineage, and loud refusal beyond its horizon.
_S271 (ruling R-55) added the transport act_: alma's TRANSPORT-1/2 runs
real bytes on minerva's codecs (the registry records the observed shape
under the Polis S3 waiting rule; the work was uncommitted in their tree
at audit time, so the pins and both fired gates wait on the landed
commit),
and its two answered sweeps are this axis's consumer numbers now: boundary
wall time linear in residue at 3.0 to 3.5 microseconds per swept locus
(30.9 ms at the full recorded document, so their ruling forbids the
interaction thread, co-signing R-54's schedule principle), and per-locus
cost flat through sixteen members (the all-to-all bookkeeping term
invisible at editor scale, leaving the slowest member's silence the real
roster ceiling, which a synchronous harness cannot observe).
_S272 (ruling R-56) activated on alma's same-day response_: the
canonical `Metatheses` frame shipped (R-55's timing gate refined: the
layout is minerva's own spelling, the registry pin still waits on the
landed commit), the fused transition became the consuming
`into_transition` door, and the declaration-scheduled recipe's safety
half became `EpochPreparation`; the epoch-frame charter's joint design
session still waits for alma's landed evidence commit and versioned
event table (their nine-event inventory and version discipline arrived
and read sound, with one correction owed back: allocator high water
and clock evidence are not `Epochs` state and belong to the caller's
own persistence). _S275 armed the session's lineage half_: the
state-identity research intake (R-56 addendum; the note is local and
untracked in `docs/lit-review/`) settled the construction family
(flat canonical-bytes state digest beside a boundary lineage chain;
incremental multiset hashing declined for document identity on the
order-insensitivity evidence), recorded minerva's three recipe
amendments for the table, and fired the one minerva-owned obligation
that stands whatever the table decides: a canonical rename-map codec,
since no published system commits the old-to-new identity map at the
cut and `RefoundMap` had no wire form. _S278 (ruling R-60) discharged
that obligation ahead of the table_ on R-56's store-spelling ground:
`REFOUND_MAP_WIRE_V1` ships with the standing codec discipline (golden
fixture, shaped refusals, six proptests over earned maps, the
`refound_map_from_bytes` fuzz target), entry position carrying the new
index so cross-station renames are unrepresentable, and the S274
session now brings a landed frame while the digest suite, preimage
composition, and R-8 embedding pin stay jointly owned at the table.
_S279 (ruling R-61) fenced this axis's future replay proposals by
theorem_: the replay-summary bound (the tenth foundations note,
`docs/metis-replay-summary-bound.adoc`) proves exact summaries of
even a movement record's visible-order outcome need one bit per
move at every width-admitted scale, so none bounded in the
live-element count exists once identifier widths are parameters: an
incremental design here is prefix-shaped (build toward a witnessed
cut, the shipped staging shape), disjointness-witnessed, or carries
history-sized state, and a *sub-history* mergeable per-member
decision summary is off the table by theorem; the watched
incremental-stratum arc is prefix-shaped and untouched.
_S280 (ruling R-62) convened the table_: alma's evidence commits
landed and verified (`83fb666c`, `764d8b03`), the rhapsody v2,
snapshot v1, have-set, and stamp embeddings entered the R-8 registry
as transport protocol contract, `Metatheses::encoded_len()` shipped
on alma's live preflight ask, and minerva's half of the table went
back as the joint-table reply letter (assents, sharpened cells, the
lifecycle-record-frames offer, the concrete lineage tuple).
_S281 (ruling R-63) closed it_: alma's ack landed executable
(`b150a2b8`, `5aebe4d5`), the presence counter was assented as
minerva's own S275 scope, the frozen table is PRD 0025, the
metatheses pins fired, and the five lifecycle record frames are the
chartered S284 program (renumbered by ruling R-64 and the intervening
R-65 release, whose sessions took
S282 for the RQ2 brief and the declaration-oath proof).
_S284 (ruling R-67, run after S285 under the reserved number) landed
the program whole_: the five frames in `src/metis/epoch/wire/` with
frozen layouts (PRD 0025 section 6's layout record), report-record
decode forms, the zero-allowance gap-free cut embedding, the two
retained seal sets distinct with the R4 displaced-declaration
fixture in golden bytes, and five fuzz targets. Alma `4060ab6b`
pinned kinds 5 through 7, and `806d4ecf` pinned kinds 8 and 9 when
the checkpoint pair entered Session Hello v3. S327 mirrors Alma's
worked `P`, `S`, `M`, `A`, and `N` rows in Minerva's lifecycle suite.
S328 pins the profile fork at Alma `1454e905`: crash-only retains that
exact nine-kind registry and fixture, while Byzantine Hello v4 adds the
205-byte kind 10 v1 attestation and requires the ordered
notice/attestation/checkpoint triple. The new row is Alma-owned and does
not widen Minerva's five lifecycle frames.
_TRANSPORT-18 (`49c11873`) supplies the phase-split field number:_
reviewed interaction-thread maxima of 72.291 and 91.667 microseconds
against 37.014 and 34.944 millisecond background fold-through-install
boundaries, with exact counts and bytes for all nine event kinds.
This favors the S270 scheduled recipe over the retired rebuild and
fires no new Minerva performance mechanism. *The epoch-ledger snapshot fired by
the same letter is built (S273, ruling R-57)*: `Epochs::snapshot()` /
`Epochs::rehydrate` with the canonical budgeted v1 frame, the open
window preserved whole across restart, the witnessable machine
invariants re-proven at decode (`InvalidState`; the unproven residues
are traced harmless in R-57's counterweight), decoded
bytes never a machine or an earned witness (`Adopted` /
`SealedEpoch` stay door-only; rehydration is the one explicit
local-trust decision and validates the caller's roster and horizon
against the checkpoint), and the charter's open question answered on
cost shape plus the S275 intake's diskless-recovery caveat: in-flight
rounds ride whole, the affine witness is re-earned through `adopt`.
Its storage-contract pin fired at alma `f37c3245`: a private, atomically
replaced owner record persists the bounded canonical ledger, then restore
requires a pending certificate-bearing checkpoint's delta generation to
equal the ledger generation and binds checkpoint lineage to the separately
stored proof. The ledger bytes are not certificate-covered, and Alma does
not grant either section authority in isolation. Alma `a813c4ee` closes the
restored-history gap before outbox replay or owner authority escapes:
ordinary checkpointed states require exact bounded-history equality, while
the durable-seal-before-checkpoint window permits exactly one newest ledger
seal beyond the proof under its generation and horizon rules. Mismatch is
`EpochWindowInstallError::LedgerProofMismatch`. Alma `9d035920` shares that
classifier between write and restore and falsifies an unrelated retained
proof beneath a canonical two-epoch pending ledger. Alma `a6b9e29d` then
replaces independent checkpoint flags with the closed `ALMAEW05` lifecycle,
preflights the bounded successor owner image before view mutation, and
retains the predecessor batch until every immutable-roster slot has a
durable authenticated-state receipt. Alma `728aa945` executes the remaining
schedule across a real process exit and fresh reopen: exact owners mint
move-only recovery capabilities, the headless adapter restores without
local re-authorship, Hello cannot release retention, and ordinary
bidirectional anti-entropy both opens the owners and carries new edits whose
dots exceed restored history. This closes the TRANSPORT~1 stage-4 record
without a Minerva implementation signal. Post-release body availability,
membership, and bootstrap policy remain B5-or-later caller work.
The plane-family question (a warning, not an avenue):: The stratum and
consignment hardcode the two document planes (text and movement). A
consumer with more epoch'd planes (marks, a `Node` tree, a cursor pair
it chooses to sweep) will want the boundary generalized over a family
of stores. *Intuition for that day:* the temptation will be a
`DotStore`-family trait threaded through stratum, shadow, and consignment;
resist it until the consumer's planes are on the table, because the
carry semantics are per-plane (the text plane re-spells, the movement
plane rebirths empty, a mark plane would re-anchor through
`anchor_dots`, and no generic trait knows which is which). The lawful
generalization is more likely a per-plane carry vocabulary than one
abstraction; carving it early is the seam-nobody-called-through
failure the μή names.
Byzantine checkpoints (the R10 pointer):: Deliberately unbuilt on this
side, and since 2026-07-19 no longer consumerless: alma's
`src/byzantium/`, re-founded 2026-07-20 as their BYZANTIUM-3 on their
live line (the earlier BYZANTIUM-1/2 commits are stale dangling
hashes on a retired branch, uncitable), founds the seam's value types
as pure walls, Ed25519 station attestation over a
configuration-and-lineage-bound v2 attestation preimage, whole-record
certificate verification, and two-attestation equivocation evidence,
with BYZANTIUM-4 adding durable seal recovery and stable-before-attest
retention. Alma `1454e905` (BYZANTIUM-5) crosses the first wire wall:
a typed Byzantine carrier owns one exact certified roster, binds its
configuration in Hello v4, and carries kind 10 as the middle member of an
ordered notice/attestation/checkpoint triple. Structural decode grants no
trust; the exact roster verifies the envelope-bound station claim against
the receiver's locally durable checkpoint subject. Crash-only Hello v3 and
kinds 1 through 9 remain byte-stable. This is attestation carriage, not
quorum-certified or freshness-gated bootstrap; those remain Alma B5/B6. The
classical
`2f + 1`-of-`3f + 1` slogan is the worst-case reading of the
threshold the consumer actually adopted: a quorum `Q = (n + f)/2 + 1`
derived from the exact roster `n`, so an honest supermajority
intersects on any concrete committee, not only at `n = 3f + 1`. The
foundation stands: `refound`'s determinism means honest holders
compute matching checkpoint digests, and the consignment makes the
opening base a deterministic function of the sealed window. S287
sharpens the future wrapper's two non-negotiable boundaries: sign a
domain-separated canonical tuple of the exact snapshot and
lineage-proof frames, with honest signers checking their semantic
agreement, because the node digest omits retained sets; and treat
freshness as caller policy, with only a returning member's durable
last-sealed generation available as an in-band floor. S292 closes
the epoch machine's half of the first boundary from the other
direction: `Epochs::bootstrap` constructs the recognizer horizon
from the verified proof itself, so no separately installable
epoch-ledger snapshot exists on the bootstrap path and the pair
binding matters only for the carried document state (alma's `C`
digests the whole payload tuple, which satisfies it). Certificates
may outlive swept history as equivocation evidence. S294 (ruling
R-76) dissolves alma's one open Minerva-owned ask (a local
seal-rehydration door for a caller crashed between its durable seal
and its checkpoint mint) into reads, not a witness mint:
`Epochs::newest_sealed` hands back the re-proven newest seal (also
the R-69 freshness floor, now stated in checkpoint terms: a seal
names its completed generation, an installable checkpoint its
successor, so refuse below the live `generation()`),
`Epochs::{generation, roster, horizon}` mirror the snapshot's
configuration reads, and `SealedEpoch::candidates` restores
wire-twin symmetry so a certificate binds both retained sets from
the live entry; the snapshot codec now also refuses a sealed join
covering an off-roster station, closing the crafted-local-checkpoint
hole. B4 needs no additional Minerva surface: the caller's profile enters
its own lineage and checkpoint digest while Minerva preserves the resulting
node opaquely. Certificate retention, freshness policy, equivocation
operations, and membership action remain caller or operator work.
*S332 (ruling R-82) walks alma's landed B5 rewrite (`1d845cf6`) against
the trust charter and the gate does not fire.* Certificate retention is
caller bytes over a caller digest; freshness-gated installation is
already R-69's floor through `newest_sealed`; successor-monotone
recovery *is* the `Epochs::bootstrap` path; the availability capability
they name is correctly caller-owned, and Minerva refuses its twin by
R-51 extended (no witness for a body the crate never holds); and the
cross-member agreement of the certified sets, which the whole quorum
argument rests on, is already pinned by the fleet suite's whole-`Epochs`
equality across the roster. *Intuition for the session after B5 lands:*
the one Minerva-owned hazard is not in any of those, it is in the
retention *vocabulary*. B5 consumes `Epochs::horizon` "for the retention
window" while stating a release rule over checkpoint bodies, and those
are different objects: the horizon is a transport fact, and bootstrap
verdict parity rests on the coverage a proof supplies rather than the
horizon a joiner declares. A trimmed proof buys a bounded, fail-closed,
non-self-healing recognizer hole (now pinned, with its exact closure at
`horizon - |proof|` further seals), so the rule to hold them to is that
releasing a body must not release its seal record,
xref:metis-checkpoint-availability.adoc[the eleventh foundations note]
carries the argument, and the reply letter that carries it back to alma
is local and untracked in `docs/miscellany/`.
== Anti-avenues: what not to build
Standing refusals, each with its recorded ground. A future session tempted by
one of these should read the citation and then not build it.
* *A disjunctive gate `Or<A, B>`.* Provably unsound against the dynamic gate
contract (`advance` folds only genuine releases); the gate algebra is closed
under `And` and `MapDep` only (the gate-algebra note; `todos.adoc` non-goals).
* *A first-party `Participation` gate.* Ruling R-4: the moment minerva ships
one it owns someone's quorum semantics forever. A caller's release-driven gate
composes as `And<Causal, CallerGate>`.
* *A membership protocol, epoch manager, or failure detector.* Axis 4; the
roster is a constructor argument.
* *A deps-bound `try_observe` variant.* Axis 6; no local ground truth exists,
so the bound would be theater. The defense is the composition discipline.
* *In-place wire-format evolution.* Axis 1; frames are byte-identity contract.
Sibling codecs only, coordinated bumps only.
* *A configurable byte order, or any pluggable serialization.* Ruling R-58:
the family is big-endian permanently. A knob would alias identity (one
value, two encodings kills the canonical bijection, the content-hash and
digest-preimage uses, and the re-encode fuzz invariant), move the meaning
of bytes out-of-band, and double every fixture and corpus, while the
decode-side win is nonexistent (validating parsers pay a `bswap` inside
validation cost) and the byte-string wins are real (memcmp order is
causal order for stamps and preserves the numeric order of dot rows). A
measured native-order need is a different artifact: an R-8 sibling codec
through the R-6 test, never a parameter.
* *A first-party `Station` wrapper before the third independent hand-roll.*
Ruling R-3; the count stands at one, and the named watch-point declined.
* *Proofs for the application machines.* Ruling R-9's exclusion list.
* *Framework drift in any form*: owning control flow, threads, I/O, or the
caller's aim. The thesis sentence ("the machine never chooses") is the test
every new surface must pass; PRD 0008 is its roadmap statement.
== Maintaining this map
Re-walk the distances after every consumer intake and every landed slice; move
markers, do not re-litigate rulings (edit those in place in
`owner-comments.adoc` per its convention). When an avenue fires, its entry here
shrinks to a pointer at the PRD or slice that absorbed it; when a new avenue
appears, it enters with signal, distance, and intuition or it does not enter.
Candidates that are scoped but *signal-less* live one step upstream, in
xref:target_arch/imagined-primitives.adoc[the imagined-primitives charter]
(S88): question, object, algebra, and hazard worked out, waiting for a signal;
the day one appears, the family enters here citing that charter.
The measure of this document is the same as the glossary's peristyle criterion:
an entry earns its place by changing what a future session does, never by
recording that something was considered.