minerva 0.2.0

//! The fleet: the epoch protocol's end-to-end assurance rung.
//!
//! Every existing epoch pin is either single-machine exhaustive
//! (`tests/epoch/` permutes decision-phase events on one honest fabric),
//! a bounded oracle (`tests/epoch_refound/`), or a per-boundary example
//! (`tests/epoch_shadow/`). Nothing yet runs the *whole shipped stack*,
//! causal pairs, `Stability`, `Epochs`, the stratum, the shadow, the native
//! `EpochGate`, and the seal, across several full replicas under an
//! adversarial delivery schedule. This module is that instrument: a
//! deterministic, seed-replayable fleet whose replicas are composed entirely
//! from shipped parts (the studio discipline), driven through complete epoch
//! lifecycles with reordering, duplication, and partitions, and checked
//! against the laws the charter states fleet-wide: one winner per
//! generation, projections identical at the seal, every read a pure function
//! of the delivered set, replays absorbing or refusing identically at every
//! replica.
//!
//! # The consumer recipe the harness encodes
//!
//! The replica half of this module is deliberately consumer-shaped: it is
//! the executable record of the duties an epoch-adopting consumer owes,
//! discovered by composing the shipped pieces end to end. PRD 0024 stage
//! four (the payload translation read) will be designed against this
//! record. The duties, each pinned by a scenario below:
//!
//! * *Every state transition mints a dot.* The stability witness ranges
//!   over dots, so an undotted retraction cannot be classified against an
//!   epoch boundary (stratum or window?); replicas would rebuild different
//!   sealed strata and freeze different maps. Deletes here mint a born-dead
//!   marker dot beside the superseded target
//!   (`boundary::classification::an_undotted_retraction_cannot_be_classified_at_the_boundary`).
//! * *The have-set counts event dots, not context spillover.* A delete
//!   delta's context names its superseded target; folding that context into
//!   the delivered have-set would raise the floor past events never
//!   delivered as deltas, and the stratum rebuilt at such a floor diverges.
//!   The transport therefore names its event dots on the envelope, exactly
//!   as the PRD 0007 envelope carries its stamp.
//! * *Declare the basis; dry-run the fold before declaring.* The vacuity
//!   half of the declare-time duty ("witnessed is not risen": a fresh
//!   tracker witnesses the bottom cut) moved into the mechanism as ruling
//!   R-40's `EpochUnrisen` refusal: both `Epochs` doors take the
//!   generation's base frontier (`Replica::base_frontier`, bottom at birth
//!   and the seal annex's gap-free floor thereafter) and refuse below it.
//!   The closure half stays the declarer's dry-run: a witnessed,
//!   basis-covering watermark can still fail to be causally
//!   self-supporting, a below-cut delete of an above-cut target putting
//!   above-cut context in every rebuilt stratum, and `EpochStratum`
//!   refuses it (`BeyondCut`) at every replica identically. The declarer
//!   runs the same checks on its own rebuild first and waits for the
//!   watermark to rise instead of opening a window no one can adopt
//!   (`boundary::classification::a_witnessed_cut_can_still_refuse_the_stratum`).
//! * *The stratum is rebuilt, never snapshotted.* A live pair mixes sealed
//!   and window state; the fold input is the generation's base state plus
//!   exactly the logged deltas whose event dots the winning cut covers.
//!   Pair-merge idempotence makes the rebuild insensitive to how much of
//!   that traffic the base already absorbed.
//! * *The seal takes the consignment.* At the seal the shadow is consumed by
//!   [`EpochShadow::consign`], and its output is the next generation's
//!   base pair whole: the final reading re-spelled through the frozen map
//!   (window births woven at their judged places, moved images where the
//!   old replay put them, window-deleted images kept as order tombstones
//!   for the native anchors that still name them), with both contexts
//!   carrying every window event dot's image so the floors are born
//!   gap-free. The door derives the generation's protocol-plane dots from
//!   the seal witness itself (`SealedEpoch::declaration_dots`) and
//!   verifies that the shadow's contexts plus that record cover the
//!   sealed join, no less and no more, before folding; nothing
//!   caller-claimed enters the check, and the replica pins the opening
//!   read equal to the frozen projection
//!   (`scenarios::window_births_and_moves_cross_the_seal_alive`, plus the
//!   per-seal assert in `Replica::try_seal`).
//! * *Native movement testimonies wait for the seal.* Movement acceptance
//!   depends on the whole incumbent topology, and the consignment re-spells
//!   exactly that topology, so a native move judged against the pristine
//!   plane can flip to a cycle-former against the consigned base (the
//!   S213 exposure one plane over, pinned in
//!   `epoch_shadow::a_window_move_can_flip_a_native_move_verdict_hence_the_deferral_duty`).
//!   The window is bounded (two watermark rounds), so movement intents
//!   queue caller-side and mint after the seal against the settled base;
//!   the replica's native alphabet is insert and delete by this duty,
//!   not by omission.
//! * *Retirement acknowledgements ride a cut and count only when covered.*
//!   An acknowledgement claims "I applied these removals"; every write its
//!   sender minted while a removed element was still visible to it precedes
//!   the acknowledgement, so it sits inside the sender's own floor. The
//!   receiver counts the acknowledgement only once it has delivered that
//!   floor (`Note::Retire`'s `at` cut, parked until covered), or an
//!   in-flight anchoring weave strands at the early condenser
//!   (`boundary::retirement::a_retirement_acknowledgement_counts_only_when_its_cut_is_delivered`).
//! * *A condense claim is fleet-applied before writing resumes, OR the
//!   writers are disciplined.* The cut-gated meet proves every member
//!   applied the removals; it cannot promise nobody writes against a
//!   tombstone again, because the visual-insert rule anchors through
//!   tombstones by design. A weave minted after its station's
//!   acknowledgement lawfully anchors a tombstone at any replica that has
//!   not excised it and dangles at any that has
//!   (`boundary::writer::a_weave_racing_a_partial_condense_strands_its_anchor`),
//!   so under the plain weave the claim needs epoch-shaped coordination:
//!   every replica excises before any new weave mints, and the fleet
//!   condenses whole at settled points, standing in for the consumer's
//!   apply round. The S224 arm records the weaker sound license (ruling
//!   R-42, the excision intake's H1): treat the station's own published
//!   acknowledgement as a quiescence oath and choose anchors in the oath
//!   plane (`Replica::insert_disciplined`), and the cut-gated meet alone
//!   licenses per-replica condense on local evidence
//!   (`boundary::writer::the_writer_discipline_unstrands_the_racing_weave`,
//!   `properties::a_disciplined_fleet_condenses_on_local_evidence_and_converges`).
//!   The oath binds on `acked`, never the gathered meet
//!   (`boundary::writer::the_discipline_binds_on_own_acknowledgement_not_the_meet`),
//!   and the price is placement, not convergence: the rebound weave
//!   forfeits the retired subtree's sibling rank contest
//!   (`boundary::writer::the_discipline_prices_placement_not_convergence`).
//!   Replays and context-only deltas stay lawful throughout either way
//!   (the lifecycle scenario's duplicate re-learn).
//! * *Surviving testimony anchors are retention pins.* A movement
//!   testimony's placement anchor is withheld from the acknowledgements
//!   while the testimony survives: excising it would silently re-decide
//!   the move, a GC that moves text. The dotted orphan retirement releases
//!   the pin, so the hygiene lifecycle is pin, excise the target, retract
//!   the testimony under its marker, unpin, excise the anchor
//!   (`scenarios::the_hygiene_lifecycle_pins_excises_and_crosses_the_boundary`).
//! * *Retirement evidence is generation-scoped.* The re-foundation
//!   compacts survivors into `1..=n`, so the next plane recurs small
//!   numerals; a tracker carried across the seal would license excising a
//!   recurring dot the new round never vouched for
//!   (`boundary::retirement::retirement_evidence_is_generation_scoped`). The tracker
//!   rebuilds at every seal, and old-generation acknowledgements drop.
//! * *The condense-time testimony retirement mints a marker, requires
//!   removal evidence, and its priority is honesty about scope.* The
//!   fleet retires orphaned testimonies as a dotted old-plane delta, and
//!   orphanhood is target-in-context beside locus-gone, never locus
//!   absence alone: a testimony can outrun its target's weave, and
//!   retiring it would erase a valid in-flight move
//!   (`boundary::retirement::an_outrun_testimony_is_not_an_orphan`, the
//!   review-caught hazard). For
//!   *orphaned* targets the undotted in-plane shape happens to be
//!   boundary-neutral (an invisible target is swept wholesale either way);
//!   the divergence lives in undotted retirement of *placement-relevant*
//!   testimonies
//!   (`boundary::classification::an_undotted_testimony_retirement_cannot_be_classified_at_the_boundary`),
//!   which is the recorded future undo path. The marker keeps the
//!   retirement uniform with every other state transition and its arrival
//!   floor-visible.
//!
//! # The rehydration recipe (the crash-restart arm)
//!
//! Since S264 (ruling R-51, on the durability-and-recovery intake) the
//! replica models its consumer's durable store explicitly: a `Journal`
//! holding one checkpoint per seal (the generation, the consigned base
//! pair, the sealed lineage, the allocator basis) plus every fenced note
//! since, in handled order. The recipe's one law is *stable before
//! emit*: the fence runs before anything leaves the outbox, so nothing a
//! replica has said can outrun what its journal can re-derive. Crashing
//! loses exactly the volatile buffer (receipts since the last fence),
//! and [`Replica::rehydrate`] is a pure replay of the journal through
//! the ordinary inbound door, no second semantics; the `resync` repair
//! lane (peers re-serve logs and re-state their idempotent round
//! positions, a sealed window's adoption round reconstructed from the
//! lineage's sealed join) restores whatever the crash silenced. The
//! lane is *bidirectional*, because a crash can also land between the
//! fence and the transport post: a durably minted note may never have
//! reached the fabric, and the journal, not the dead outbox, is the
//! source of record for what the replica has said
//! (`scenarios::recovery::a_persisted_but_unsent_mint_reaches_the_fleet_through_repair`).
//! And the *bounded-record rule* keeps repair idempotent in cost as well
//! as effect: a redelivered data note still folds (a condensed tombstone
//! may lawfully re-learn), but only a novel note appends to a log or
//! fences into the journal, fencing is effect-based for protocol notes
//! (a note buffers only if dispatching it changed the round state it
//! addresses or parked), and a note that outruns its record parks once
//! (an exact duplicate re-teaches nothing), so redelivery, duplication,
//! and repeated crash-repair cycles never compound the record
//! (`scenarios::recovery::alternating_restarts_keep_the_record_bounded`,
//! `boundary::out_of_reach_protocol_notes_park_once_and_cure_on_the_prerequisite`).
//! The duties, each priced by a falsifier when violated:
//!
//! * *Fence the mint before the note posts.* The dot allocator
//!   re-derives from the journal, so an unfenced emitted mint is reused
//!   after restart and one identity names two payloads forever, the one
//!   crash hazard that is corruption rather than lag
//!   (`boundary::durability::an_unfenced_mint_reused_after_restart_forks_identity`).
//! * *Fence the oath's basis before acknowledging.* A retirement
//!   acknowledgement binds the writer discipline; forgetting it after
//!   restart re-anchors a dot the fleet lawfully excised and the weave
//!   strands, the R-42 divergence reopened by amnesia
//!   (`boundary::durability::an_unfenced_oath_lets_a_restarted_writer_strand_its_weave`).
//! * *Report only the fenced floor.* Every peer's tracker folds by join,
//!   so a post-restart regression is absorbed silently (the masking is
//!   the price of order-robustness, PRD 0011 R8's second face); the
//!   declaration licensed on the masked claim opens a window the
//!   amnesiac cannot rebuild. Under the roster-meet gating this fails
//!   closed, a wedge cured by repair, never corruption
//!   (`boundary::durability::a_report_beyond_the_fenced_floor_wedges_the_window_until_repair`).
//! * *Checkpoint at the seal.* The consigned base pair, the sealed
//!   lineage, and a clock high-water are compaction output: the swept
//!   history that could re-derive them is gone fleet-wide (the
//!   re-foundation re-bases ranks, so the sealed window's spoken stamps
//!   survive in no walkable plane), so they must be durable before the
//!   replica participates in the new generation. The checkpoint moment
//!   is the seal itself, where every piece is computed anyway.
//! * *Recovery is replay plus repair, and the witness is re-earned.* The
//!   [`Adopted`](crate::metis::Adopted) witness is deliberately never
//!   persisted: rehydration re-runs `adopt` over the rebuilt record and
//!   earns it again, the replayed allocator advances past every own
//!   dot before any journaled protocol note can re-run the adoption,
//!   and the clock re-derives from the checkpoint watermark, the
//!   journaled notes' carried stamps, and the rebuilt planes before
//!   anything can mint, so no post-restart stamp undercuts a spoken one
//!   and repair re-serves under original stamps only
//!   (`scenarios::recovery::a_mid_window_crash_rehydrates_and_the_fleet_seals`,
//!   `scenarios::recovery::a_restart_never_undercuts_a_spoken_stamp`,
//!   `properties::any_schedule_with_crashes_rehydrates_and_converges`).
//!
//! The asymmetry the falsifiers pin is the arm's finding: because every
//! irreversible step in this protocol waits on a roster-wide meet,
//! losing *receipts* is always a liveness event, repairable by the
//! consumer's anti-entropy; only losing *own testimony* corrupts. The
//! minimal durable set is exactly what the replica has already said (its
//! mints, its oath, the bases of its round positions, the checkpoint it
//! sealed), and received-data durability stays a batching policy.
//!
//! One scope honesty note: the journal is deliberately an in-memory
//! *model* of the duties (which facts must be durable before which
//! emission), not a persistence surface. Since S273 (ruling R-57) the
//! epoch-ledger half of the seal checkpoint has its canonical codec
//! ([`Epochs::snapshot`](crate::metis::Epochs::snapshot) /
//! [`Epochs::rehydrate`](crate::metis::Epochs::rehydrate) over
//! [`EpochLedgerSnapshot`](crate::metis::EpochLedgerSnapshot), carrying
//! the generation, roster, horizon, open window, and sealed lineage);
//! the consigned base pair has the rhapsody snapshot codec, and
//! spelling the durable store's outer bytes (the authenticated
//! checkpoint record) stays the consumer's, whose embedding of the
//! ledger frame is the coordinated R-8 event (PRD 0024 R7).
//!
//! # The bootstrap joiner recipe
//!
//! Since S293 (ruling R-75), the fleet also exercises the S292 admission
//! door end to end. A joiner consumes two distinct authorities: a local
//! data-plane checkpoint exported exactly at a seal, and a certificate-
//! verified [`LineageProofRecord`](crate::metis::LineageProofRecord) whose
//! `SealRecord::from_sealed` entries install only the recognizer horizon
//! through [`Epochs::bootstrap`](crate::metis::Epochs::bootstrap). The
//! constructor rejects a station outside the fixed roster and a checkpoint
//! whose generation disagrees with the proof. Live floors, round state, and
//! [`Adopted`](crate::metis::Adopted) never cross either input; the ordinary
//! repair lane supplies them. The scenario pins replay-verdict parity,
//! participation in the next seal, and the R-71 edge where a later crash
//! parks a new-generation report until sealed-round restatement repairs it
//! (`scenarios::bootstrap::a_bootstrap_joiner_enters_the_fleet_and_crosses_the_next_seal`).
//!
//! Since S332 (ruling R-82) the recipe also pins what that parity rests
//! on. Verdict parity is a property of the *proof's coverage*, not of the
//! declared horizon: the door refuses a proof longer than the horizon and
//! accepts any shorter one, so a caller that trims its proof admits a
//! joiner whose old-addressed doors part from every incumbent's below the
//! trim. They part fail-closed ([`EpochRefusal::BeyondHorizon`](crate::metis::EpochRefusal),
//! the machine declining to guess, on both `recognize` and `deliver`), the
//! document plane stays converged throughout, the hole never heals by
//! sealing forward, and it closes only once eviction has brought both
//! sides to the same newest `horizon` generations
//! (`scenarios::bootstrap::a_truncated_bootstrap_proof_holds_a_bounded_recognizer_hole`).
//! The consumer-facing reading is
//! xref:docs/metis-checkpoint-availability.adoc[the availability note]:
//! releasing a checkpoint *body* must not release its *seal record*.
//!
//! # The admitted joiner recipe (recorded membership)
//!
//! Since S343 (ruling R-90, PRD 0028's fleet carriage) the recipe carries
//! *membership change* end to end. The operator's decision is
//! [`Replica::open_arrival`]: open the machine-held round over the newest
//! seal and endorse in one act, journal the endorsement before it travels
//! (the R3 mint duty), then run the full parked-note drive, because a
//! peer's early word parks on `NoRound` and this act is what unparks it.
//! The winner's declaration carries the completed round's boundary; the
//! seal widens the machine's roster; and the recipe reads its own roster
//! back from the record just sealed, *before* the stability and
//! retirement trackers rebuild, so both families widen in the same act
//! (the R-87 question: retirement evidence widens with the roster, and
//! the meet only ever lowers). The joiner enters through
//! `joiner_checkpoint_for`, the checkpoint re-stamped for a station that
//! never held one --- allocator at the station's own plane coordinate,
//! attested departures carried as the seat's world, bare abandons
//! deliberately not --- and the bootstrap door derives its roster from
//! the walked proof (PRD 0028 R4). An attestation crossing any seal
//! re-declares at the evictee's compacted prefix in the consigned base,
//! never at bottom: the bottom carry understated a surviving evictee's
//! coordinate and wedged the second post-attestation seal, the S339
//! latent defect this recipe's exhibits caught
//! (`scenarios::arrival`, nine exhibits; the minimal reproduction is
//! `an_evictees_survivors_cross_the_second_boundary`).
//!
//! # Scope
//!
//! Old-addressed *births and moves* in flight across the boundary are
//! exercised end to end since the stage-four document-plane carry landed
//! (ruling R-50): the shadow judges them in the old topology, the seal
//! takes [`EpochShadow::consign`] as the next generation's base, and the
//! generated law drives the full laggard alphabet (insert, delete, move)
//! through open windows under reordering, duplication, and severance.
//! Crash-restart rehydration is in since S264 (the recipe above); the
//! S293 bootstrap arm is replica admission from sealed state within a
//! fixed roster, and membership change itself is in since S343 (the
//! admitted-joiner recipe above). The
//! consumer-payload half of stage four stays gated on the first adopting
//! consumer: external references (cursors, held mark identities, content
//! hashes) re-translate through the consignment's retired map, whose retention
//! and frame family are the consumer's (PRD 0024 R7). Payload translation
//! for caller planes beyond the two carried here stays out with its own
//! gate. The membership schedule tape has driven admissions, joiner
//! bootstrap, and departure-attestation races since S347 (ruling R-93), as a
//! sibling interpreter so the epoch tape's existing bytes remain stable.
//!
//! # Where this harness runs
//!
//! Under `cargo test`, whole. Under `--cfg fuzzing` (cargo-fuzz's build
//! flag, which no Cargo feature can reach), the fabric, the replica
//! recipe, [`tape`], and [`membership_tape`] compile without the scaffolded
//! proptest suites, so the `epoch_schedule_tape` and
//! `membership_schedule_tape` fuzz targets drive *this* recipe rather than a
//! copy of it (S331/R-81 and S347/R-93, on the path R-71 reserved).
//! That exposure is the reason a change here can be felt in two places:
//! the always-on suite and the coverage-guided leg.

// A fuzz build compiles this subtree without its `cfg(test)` suites, so
// the recipe surface those suites drive (scenario readers, durability
// counters, the seeded interpreter) is present and uncalled. The allow is
// scoped to exactly that build: under `cargo test` dead harness code stays
// a warning, which is how a retired defense gets noticed.
#![cfg_attr(all(fuzzing, not(test)), allow(dead_code))]

extern crate alloc;

// The fabric, the replica recipe, and the tape compile under `--cfg
// fuzzing` too (the libFuzzer leg drives them; ruling R-71, S331); the
// proptest-driven scaffolded suites stay test-only, so a fuzz build
// resolves no dev-dependency.
#[cfg(test)]
mod boundary;
#[cfg(test)]
mod byzantine;
mod fabric;
pub(in crate::metis) mod membership_tape;
#[cfg(test)]
mod properties;
mod replica;
#[cfg(test)]
mod scenarios;
#[cfg(test)]
mod sweep;
pub(in crate::metis) mod tape;

use alloc::collections::{BTreeMap, BTreeSet};
use alloc::vec::Vec;
use core::num::NonZeroUsize;

use crate::metis::{
    Dot, EpochAddress, LineageProofEntry, LineageProofRecord, SealRecord, SealedEpoch,
};

use fabric::{Fabric, Note, OldDelta};
use replica::Replica;

/// Exports the retained recognizer lineage in its authenticated-record
/// shape. The node values are opaque to minerva; certificate verification
/// belongs to the consumer boundary ahead of `Epochs::bootstrap`.
fn lineage_of(replica: &Replica) -> LineageProofRecord {
    let entries = replica
        .epochs()
        .sealed()
        .map(|sealed| LineageProofEntry::new(SealRecord::from_sealed(sealed), [0u8; 32]))
        .collect();
    LineageProofRecord::try_new(entries).expect("a retained lineage is consecutive")
}

/// Crashes replica `id` and rebuilds it from its journal alone: every
/// volatile receipt is lost, everything fenced replays through
/// [`Replica::rehydrate`]. In-flight fabric traffic survives (a crash
/// stops a station, not the network), so redelivery to the restarted
/// replica is lawful and exercised.
fn crash(fleet: &mut BTreeMap<u32, Replica>, roster: &[u32], horizon: NonZeroUsize, id: u32) {
    let journal = fleet
        .get(&id)
        .expect("the driver crashes roster members")
        .journal()
        .clone();
    let _ = fleet.insert(id, Replica::rehydrate(id, roster, horizon, &journal));
}

/// The repair lane: every peer re-serves its logs and re-states its
/// idempotent round positions, targeted at the restarted station, and
/// the restarted station re-serves its own durable record back to every
/// peer. The lane is bidirectional because a crash can land between the
/// fence and the transport post: a durably minted note may never have
/// reached the fabric, and after a crash the journal, not the dead
/// outbox, is the source of record for what the replica has said (the
/// persisted-but-unsent scenario). The consumer's anti-entropy duty made
/// explicit; the notes enter the scheduled pool, so repair interleaves
/// with live traffic adversarially, and the bounded-record rule at every
/// receiving door keeps repeated repairs from compounding anything.
fn resync(fabric: &mut Fabric, fleet: &BTreeMap<u32, Replica>, id: u32) {
    let restarted = fleet.get(&id).expect("the driver repairs roster members");
    for (&peer, replica) in fleet {
        if peer == id {
            continue;
        }
        let mut serve = Vec::new();
        replica.reserve_logs(&mut serve);
        replica.restate(&mut serve);
        for note in &serve {
            fabric.send(peer, id, note);
        }
        let mut announce = Vec::new();
        restarted.reserve_logs(&mut announce);
        restarted.restate(&mut announce);
        for note in &announce {
            fabric.send(id, peer, note);
        }
    }
}

/// A fresh fleet over `roster`, every replica retaining `horizon` sealed
/// epochs.
fn fleet_of(roster: &[u32], horizon: NonZeroUsize) -> BTreeMap<u32, Replica> {
    roster
        .iter()
        .map(|&id| (id, Replica::new(id, roster, horizon)))
        .collect()
}

/// Runs one local action on replica `id` and posts its outbox.
fn act<R>(
    fabric: &mut Fabric,
    fleet: &mut BTreeMap<u32, Replica>,
    id: u32,
    action: impl FnOnce(&mut Replica, &mut Vec<Note>) -> R,
) -> R {
    let replica = fleet.get_mut(&id).expect("driver targets roster members");
    let mut outbox = Vec::new();
    let result = action(replica, &mut outbox);
    fabric.post(id, outbox);
    result
}

/// Asserts every retained seal record is *determined by its own certified
/// set*: the per-replica half of agreement, checked at the record rather
/// than across the roster.
///
/// The cross-replica comparison in [`assert_converged`] answers "did the
/// members agree?" and a sealed entry is immutable once retired, so a
/// seal-time divergence does survive to it. What it cannot answer is *why*
/// they agreed, and that is the load-bearing half: a seal record must be a
/// function of the adoption round's certified join, never of the order this
/// replica happened to receive the window's traffic. Final fleet states
/// converge by law, so a closing comparison is blind to an arrival-order
/// dependence introduced upstream of it (the S331 mutation lesson).
///
/// [`SealedEpoch`](crate::metis::SealedEpoch) retains two collections and
/// only one of them wears the certification on its face. `protocol` is
/// filtered against the sealed join at `try_seal`, so its canonicality is
/// visible in the record. `candidates` is retained raw off the surviving
/// antichain, and its canonicality holds because the antichain is
/// *complete* at every latch: the latch gate is the roster-wide meet rising
/// to the confirmation join, which names every concurrent declaration's
/// dot, so no member can fix on a partial candidate set (`sweep`, which
/// freezes every replica's latch by withholding one declaration from one
/// station). Every retained candidate's author must also have reported
/// adoption for the round to complete, at an own-station counter no lower
/// than the dot it minted earlier.
///
/// That derivation has a checkable consequence, and this is it: every
/// retained candidate's dot survives the join filter, so `candidates` is a
/// subset of the same certified ledger `declaration_dots` publishes. If the
/// derivation is ever wrong, a candidate outruns the join and this fires.
/// Hooked into `assert_converged` so it rides every convergence point the
/// generated lifecycles, the addressed tape, and the fuzz target already
/// reach, rather than adding call sites of its own. It is *vacuous* at any
/// checkpoint whose lineage is empty, which is every convergence point
/// before a first seal and every one after the horizon has evicted the
/// only entry: it is a safety net over the seals that exist, not a claim
/// that seals existed.
///
/// *Claim it narrowly.* On the tree as it stands the invariant is
/// over-determined: dropping roster unanimity from the seal trigger (fold
/// present reports instead of refusing while any member is silent) makes
/// this fire, but the suite already failed the same 29 tests without it, so
/// this adds a diagnosis, not a kill. It earns its place as the statement
/// that makes the `candidates` derivation *falsifiable* rather than
/// prose-only, and as the first assert to speak when a seal outruns its
/// round. It is not a new assurance rung, and the mutant catalogue gains no
/// site from it.
fn assert_seals_certified(fleet: &BTreeMap<u32, Replica>) {
    for replica in fleet.values() {
        for sealed in replica.epochs().sealed() {
            let certified: BTreeSet<Dot> = sealed.declaration_dots().collect();
            for candidate in sealed.candidates() {
                assert!(
                    certified.contains(&candidate.declaration()),
                    "replica {}: epoch {:?} retains candidate {:?}, whose dot the sealed join \
                     does not cover",
                    replica.id(),
                    sealed.declaration(),
                    candidate
                );
            }
            // No separate winner check: `fix` picks the winner out of
            // `window.candidates` and nothing leaves that map once the
            // latch is set, so the winner is always one of the candidates
            // the loop above already covered. A redundant assert is dead
            // code wearing a defense's clothes.
        }
    }
}

/// Asserts every retained seal record was **accepted at its own
/// consignment door**: the certification duty, read fleet-wide.
///
/// `assert_seals_certified` above checks a seal record against itself. This
/// checks it against the *other plane*. A [`Consigned`](crate::metis::Consigned)
/// exists only where a replica's document plane accepted the record its
/// protocol plane retired, so the two lists agreeing is the statement that
/// no member is carrying a seal its own deliveries refuse --- which is
/// exactly the gap the durable wedge opens
/// (`fleet::byzantine::the_wedge_is_durable_and_no_shipped_door_recovers_it`,
/// where the ledger stands one generation ahead of the certified list and
/// stays there).
///
/// It is not implied by the `epochs()` equality `assert_converged` already
/// checks: that compares protocol planes to protocol planes, and this
/// compares each protocol plane to its own document plane. Non-vacuous
/// wherever any seal is retained, and honestly empty before the first one.
fn assert_lineage_was_consigned(fleet: &BTreeMap<u32, Replica>) {
    for replica in fleet.values() {
        let accepted: BTreeSet<EpochAddress> =
            replica.certified().map(SealedEpoch::declaration).collect();
        for sealed in replica.epochs().sealed() {
            assert!(
                accepted.contains(&sealed.declaration()),
                "replica {}: epoch {:?} is retained in the lineage but its consignment was \
                 never accepted, so it is not certifiable",
                replica.id(),
                sealed.declaration()
            );
        }
    }
}

/// Asserts the whole fleet has converged: same generation, same lineage,
/// same seal record (address and final projection per epoch), the same
/// current pairs, and byte-identical text frames (the wire is the
/// representation-independence witness), that each retained seal record
/// is certified by its own join ([`assert_seals_certified`]), and that each
/// was accepted at its own consignment door
/// ([`assert_lineage_was_consigned`]).
fn assert_converged(fleet: &BTreeMap<u32, Replica>) {
    assert_seals_certified(fleet);
    assert_lineage_was_consigned(fleet);
    let mut replicas = fleet.values();
    let first = replicas.next().expect("a fleet has at least one member");
    for other in replicas {
        assert_eq!(
            first.generation(),
            other.generation(),
            "replicas {} and {} disagree on the generation",
            first.id(),
            other.id()
        );
        assert_eq!(
            first.epochs(),
            other.epochs(),
            "replicas {} and {} disagree on the epoch record",
            first.id(),
            other.id()
        );
        assert_eq!(
            first.seals,
            other.seals,
            "replicas {} and {} disagree on a seal's projection",
            first.id(),
            other.id()
        );
        assert_eq!(
            first.text(),
            other.text(),
            "replicas {} and {} text pairs diverged",
            first.id(),
            other.id()
        );
        assert_eq!(
            first.moves(),
            other.moves(),
            "replicas {} and {} movement pairs diverged",
            first.id(),
            other.id()
        );
        assert_eq!(
            first.text().store().to_bytes(),
            other.text().store().to_bytes(),
            "replicas {} and {} agree logically but not byte-identically",
            first.id(),
            other.id()
        );
        assert_eq!(
            first.effective_order(),
            other.effective_order(),
            "replicas {} and {} read different effective orders",
            first.id(),
            other.id()
        );
    }
}