= Checkpoint availability: three objects, three retention duties
:toc: macro
*Status: the eleventh foundations note (S332, ruling R-82). A reference,
not a charter: nothing here licenses a slice. It owns the retention
vocabulary the Byzantine checkpoint arc needs and Minerva had never
written down, which of the three objects at a sealed boundary Minerva
retains, which it never holds, and what a caller's own retention policy
may and may not derive from `Epochs::horizon`. It was written against
alma's landed B5 plan (`1d845cf6`, read at source), whose design
consumes exactly the reads this note bounds. Every claim is marked
_derived_ (from the machine's own definitions), _tested_ (a pinned test
names it), or _cited_ (read at the named source, and theirs to own).*
toc::[]
== 1. What this note owns
At every sealed epoch boundary three distinct objects come into
existence, and the Byzantine arc gives each of them a different
lifetime:
* the *seal record*: Minerva's own retained recognizer, a
`SealedEpoch` in the lineage, exported as a `SealRecord` and carried
in a `LineageProofRecord`. Small: a winner address, a candidate set, a
canonicalized declaration ledger, and a sealed join.
* the *checkpoint body*: the caller's serialized document state at that
boundary. Large, and Minerva never holds it: the crate's contribution
is that the body is a deterministic function of the sealed window, not
that the crate stores one.
* the *certificate*: the caller's quorum-signed authenticity record
over the checkpoint digest. Minerva never holds one and has no opinion
about its verification.
The confusion this note exists to prevent is treating those three as one
retention window, and in particular deriving any of them from
`Epochs::horizon`. They are three duties with three different owners and
three different sizes, and the failure mode of conflating them is
concrete and pinned (§4).
== 2. What `Epochs::horizon` actually bounds
_Derived._ The horizon is a caller-declared constructor argument
(`Epochs::new(roster, horizon)`, the S30 capacity idiom: the bound is
mechanism, its value is the caller's fact). What it bounds is the
*recognizer lineage*: the number of sealed generations retained so that
old-addressed traffic can still be judged. At each seal the newest entry
is pushed and the lineage is truncated to the horizon from the oldest
end.
Within the horizon `recognize` answers old-addressed traffic with the
duplicate verdict or the typed `AddressMiss` violation; below it, the
machine can no longer tell duplicate from violation and returns
`BeyondHorizon` rather than guessing. `deliver` answers a redelivered
declaration the same way.
The value the caller should declare is therefore a *transport* fact:
how far back its transport can lawfully replay a frame. It is not a
storage-cost knob, not a retention policy, and not a function of how
many checkpoint bodies the caller keeps. A caller that sets the horizon
from its body-retention policy has answered a transport question with a
storage answer.
== 3. Why no availability witness can live here
_Derived._ Minerva mints witnesses for facts it can observe. `Adopted`
is affine and live-only because adoption is a live fact the crate
performs; a `Cut` is unfakeable because its constructors are a closed
honest set. Availability is not such a fact. Whether the bytes a digest
names are on some disk, and whether their holder will still serve them
when asked, are facts about the caller's storage and the network, the
crate has no local ground truth for either.
This is the S264 argument (ruling R-51) one level up. That slice refused
a library `Durable` witness on the ground that 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. An availability witness
is the same object with a longer promise attached: not "these bytes were
written" but "these bytes will be served." If the crate cannot honestly
witness the first, it certainly cannot witness the second.
_Cited (alma `1d845cf6`)._ The consumer reached the same boundary from
its own side and drew it in the same place: a `CheckpointCertificateRecord`
is durable authenticity evidence, not a timeless availability witness,
and the live capability representing local body possession under an
active retention obligation is deliberately non-serializable. That
capability is theirs. Minerva's contribution to it is determinism, the
reason a digest means anything at all, and nothing else.
== 4. The truncated-proof lemma
This is the load-bearing result, and the one a body-retention policy can
walk into without noticing.
*Lemma.* _Tested_
(`fleet::scenarios::bootstrap::a_truncated_bootstrap_proof_holds_a_bounded_recognizer_hole`).
Let a joiner be admitted through `Epochs::bootstrap` with declared
horizon `k` and a lineage proof of length `j < k`, while the incumbents
retain `i` generations, `j < i <= k`. Then:
. *Inside the proof's coverage the joiner is indistinguishable from an
incumbent.* Both old-addressed doors, `recognize` and `deliver`,
return identical verdicts for every generation the proof carries.
. *Below it they part, fail-closed.* For a generation the proof omitted,
incumbents grant the duplicate verdict while the joiner returns
`BeyondHorizon` on both doors. The joiner never absorbs blind; it
declines to judge. No replicated value diverges, the document plane
stays converged across the hole.
. *The hole does not heal by catching up.* Sealing forward never
re-acquires an omitted generation; the joiner is simply short.
. *It closes only by eviction, after exactly `k - j` further seals*, at
which point both sides hold the same newest `k` generations and answer
identically again.
_Derived_ for the closure count: the joiner's lineage grows by one per
seal to the cap `k`, so it reaches the cap after `k - j` seals; the
incumbents are at or below the cap throughout and reach it no later.
Once both are capped they hold the same newest `k` generations by
construction.
The door itself is honest at every step: `bootstrap` refuses a proof
*longer* than the declared horizon (trimming is the caller's visible
act, never a silent truncation) and accepts any shorter one, because a
short proof is exactly what a fresh-ish fleet legitimately has. What
nothing warned about is that the *supplied coverage*, not the *declared
horizon*, is what verdict parity rests on.
== 5. The consequence for a body-retention policy
_Derived from §4._ A structural release rule stated over checkpoint
*bodies*: release generation `N-1` once `N+1` is verified, freshness-
accepted, and installed, is a policy about the large object. If the
caller lets that rule govern which *seal records* it retains, then every
joiner it admits gets a proof trimmed to the same depth, and by the
lemma every such joiner carries a recognizer hole exactly as deep,
refusing lawful old-addressed traffic its peers absorb for `k - j`
generations.
The rule that avoids it is one sentence: *releasing a checkpoint body
must not release its seal record.* The two objects are wildly
asymmetric in size, a seal record is a winner address, a candidate set,
a ledger, and a join, against a whole serialized document, so retaining
seal records out to the fleet's declared recognizer horizon is close to
free even under an aggressive body-release policy. Certificate retention
and equivocation-evidence horizons remain separate again, and may
lawfully outlive both.
A caller that genuinely cannot retain seal records to the horizon has
not hit a Minerva limit; it has chosen a smaller effective horizon, and
should declare that smaller horizon fleet-wide so that no member's
verdicts depend on how it happened to join.
== 6. What this note does not decide
_Cited (alma `1d845cf6`), and theirs._ The conditional quorum argument
(that `Q > f` plus an active per-signer retention duty yields one
serving honest holder, and that without the duty a certificate proves
only that `Q` members signed a digest); whether that stronger duty is
bound to a negotiated profile, configuration policy, or attestation
version; collector topology and durable ownership; body-fetch framing;
the structural irrelevance proof a signed-but-never-certified body needs
before deletion; and the rule that withholding is telemetry rather than
transferable evidence. All of these are protocol and policy decisions in
the consumer's layer. None of them asks for Minerva mechanism, and this
note takes no position on them beyond recording that they were read.
== 7. Standing summary
* `Epochs::horizon` bounds recognizer retention, and its value is a
transport fact. It is not a body-retention window, a certificate
horizon, or a storage knob.
* Minerva retains seal records. It never holds a checkpoint body or a
certificate, and mints no witness about either.
* Verdict parity across a fleet rests on the coverage a joiner's proof
supplies, not on the horizon it declares.
* Releasing a body must not release its seal record.