minerva 0.2.0

//! The latch-cut probe: why the protocol plane has no decision space to
//! sweep, and the pin that says so.
//!
//! # What this module was going to be
//!
//! The S332 research intake recommended partial-order reduction over
//! interleavings as the next rung above the sampled tape. That was rejected
//! on the cost that actually binds (on a three-replica fleet nearly every
//! transition touches the same replica's window, so a sound dependence
//! relation buys almost no reduction), and the counter-proposal was to
//! enumerate *protocol-plane decision points* instead: for one window, the
//! only order-sensitive variable per replica looked like *the set of
//! declarations it delivered before it latched a winner*, its **latch
//! cut**. Sweeping every assignment of per-replica latch cuts would have
//! been exhaustive over that space where every other arm samples.
//!
//! # Why it is not that
//!
//! The space is a singleton. A replica cannot latch on a partial candidate
//! set, and the reason is sharper than the module doc's prose argument:
//!
//! * The latch needs the confirmation round complete *and* the stability
//!   watermark risen to cover that round's join.
//! * Each member's confirmation cut carries its own declaration dot, so the
//!   join names every concurrent declaration's dot.
//! * The watermark is the roster-wide meet, so covering that join requires
//!   *every* member to have delivered *every* concurrent declaration.
//!
//! So the candidate set is complete at every latch, fleet-wide, and it is
//! complete before any latch anywhere. There was nothing to enumerate: the
//! sweep would have had exactly one feasible combination.
//!
//! The probe that established this is kept as
//! [`a_withheld_declaration_freezes_every_latch`], because the negative
//! result is the valuable part and an unpinned negative result rots. It is
//! also the stronger statement about the seal record's collection fields:
//! `SealedEpoch::candidates` is identical at every member not because the
//! surviving antichain is order-insensitive (true, but derived, and its
//! premise is inherited from the delivery discipline) but because the
//! candidate set is *complete* everywhere before anyone latches. The
//! derivation is the fallback argument; this is the operative one.
//!
//! # What this licenses
//!
//! That the latch waits for the complete candidate set, pinned at one
//! deterministic three-station configuration. It is not a theorem and not a
//! new rung: it sits on the specification-oracle rung beside the other
//! fleet laws, a complement and never an upgrade. It does not speak to
//! crash points, which the recovery scenarios own, nor to rosters or
//! declaration counts outside the pinned one.

extern crate alloc;

use alloc::vec::Vec;
use core::num::NonZeroUsize;

use crate::metis::EpochAddress;

use super::fabric::Fabric;
use super::{Note, act, assert_converged, fleet_of};

const ROSTER: [u32; 3] = [1, 2, 3];

/// The two stations that declare concurrently. Distinct stations mint
/// distinct ranks, so the winner rule's `(rank, dot)` contest is live
/// rather than decided by the dot alone.
const DECLARERS: [u32; 2] = [1, 3];

fn horizon(depth: usize) -> NonZeroUsize {
    NonZeroUsize::new(depth).expect("a positive horizon")
}

/// Withholding one declaration from one station freezes *every* replica's
/// latch, not merely that station's: the latch cut is not a free variable,
/// so there is no decision space to sweep.
///
/// The freeze is fleet-wide because the gate is the roster-wide meet, not a
/// local read. Station 2 is missing a declaration, so its confirmation cut
/// cannot cover that declaration's dot, so the meet cannot rise to the
/// confirmation join at *any* member, so no member latches. This is the
/// same shape as the silent-member freeze, reached by withholding one note
/// rather than by severing a station: the window stays open, nothing
/// corrupts, and delivering the withheld note lets the whole fleet seal.
///
/// What it pins, and why it is worth a test rather than a comment: that
/// `SealedEpoch::candidates` is identical at every member *by completeness
/// at the latch*, which is a stronger and more local argument than the
/// order-insensitivity of the surviving antichain. Weakening the latch's
/// watermark gate would let station 2 fix on one candidate while its peers
/// fix on two, and the seal records would diverge in exactly the field
/// R-82's fifth disposition rests the Alma B5 quorum argument on.
#[test]
fn a_withheld_declaration_freezes_every_latch() {
    let mut fleet = fleet_of(&ROSTER, horizon(2));
    let mut fabric = Fabric::new(0x5EED_0C17, &ROSTER, 0);

    // Warm the watermark so the declare door's risen license is available.
    for (offset, &station) in ROSTER.iter().enumerate() {
        let _ = act(&mut fabric, &mut fleet, station, |replica, out| {
            replica.insert_visible(offset, out)
        });
    }
    fabric.drain(&mut fleet);

    // Both declare before either delivery lands: concurrent candidates.
    let minted: Vec<EpochAddress> = DECLARERS
        .iter()
        .map(|&station| {
            act(&mut fabric, &mut fleet, station, |replica, out| {
                replica.try_declare(out)
            })
            .expect("a settled watermark licenses the declaration")
        })
        .collect();
    let withheld = minted[1];

    // Everything moves except that one declaration to station 2.
    fabric.drain_selected(&mut fleet, |dst, note| {
        !matches!(note, Note::Declare { declaration }
            if dst == 2 && declaration.address() == withheld)
    });

    assert_eq!(
        fabric.in_flight(),
        1,
        "exactly the withheld declaration waits"
    );
    assert_eq!(
        fleet[&2].epochs().candidates().count(),
        1,
        "station 2 holds the partial candidate set"
    );
    for &station in &ROSTER {
        let replica = &fleet[&station];
        assert!(
            replica.epochs().fixed().is_none(),
            "station {station} latched on a candidate set that is not complete fleet-wide"
        );
        assert!(
            !replica.adopted(),
            "station {station} adopted without a latch"
        );
        assert_eq!(
            replica.generation(),
            1,
            "station {station} sealed with a declaration still in flight"
        );
    }
    for &station in &DECLARERS {
        assert_eq!(
            fleet[&station].epochs().candidates().count(),
            2,
            "station {station} holds both candidates and still cannot latch"
        );
    }

    // The withheld note lands: the fleet seals on the complete set.
    fabric.drain(&mut fleet);
    assert_converged(&fleet);
    for &station in &ROSTER {
        let replica = &fleet[&station];
        assert_eq!(
            replica.generation(),
            2,
            "station {station} crossed the seal"
        );
        let sealed = replica
            .epochs()
            .sealed()
            .next()
            .expect("the generation sealed");
        assert_eq!(
            sealed.candidates().count(),
            2,
            "station {station} retired both candidates"
        );
        for &address in &minted {
            assert!(
                sealed.contains(address),
                "station {station} dropped candidate {address:?} from the seal record"
            );
        }
    }
}