minerva 0.2.0

mod and;
mod causal;
mod fifo;
mod laws;

pub use and::{And, AndProgress};
pub use causal::Causal;
pub use fifo::Fifo;
pub use laws::{GateLawCheckError, GateLawPoint, check_gate_laws};

/// The buffer's *stability rule*: the seam an [`Ideal`](crate::metis::Ideal) runs its machine over (PRD 0009).
///
/// [`Ideal`](crate::metis::Ideal) is a general machine. It holds an event until
/// stable, releases the stable frontier in stamp-minimal order, and forgets
/// released events. This trait names only the stability rule.
/// Causal happens-before is one rule ([`Causal`]), per-source FIFO another
/// ([`Fifo`]), [`And`] composes two, and a participation or quorum watermark
/// is a caller's.
///
/// The gate is the axis *below* the frontier: when to release. The resolver
/// above it. The caller decides what the concurrent frontier becomes
/// (PRD 0008).
///
/// # The invariant: `stale` is terminal
///
/// [`Progress`](Self::Progress) is ordered by information, starts at bottom,
/// and [`advance`](Self::advance) moves it only *up*. That monotone rise is
/// load-bearing: every law here is stated against it. The shipped gates go
/// further, their progress being a join-semilattice, but the machine never
/// joins two arbitrary progresses, so that lattice shape is those gates' and
/// not the trait's.
///
/// Fix a `(sender, dep)` pair. As progress rises, a gate MUST sort each
/// progress state into three regions, and MUST report at most one region at a
/// time: *waiting*, *deliverable*, and *dead*. [`stale`](Self::stale) reports
/// the *dead* region. Three independent laws over those regions make the
/// machine safe:
///
/// * *Terminal `stale`.* `{ progress : stale(p, _, dep) }` is an up-set: once
///   stale, stale for every greater progress. That finality is what lets
///   [`insert`](crate::metis::Ideal::insert) drop a stale event, and the
///   bounded [`try_insert`](crate::metis::Ideal::try_insert) reclaim a
///   pending one, on the strength of the current progress alone.
/// * *Disjoint from [`deliverable`](Self::deliverable).* No progress reports
///   an event both stale and deliverable. The release path consults only
///   `deliverable`, so this is what stops the stale-first drop discarding an
///   event a release would have delivered.
///
/// * *Stable up-closure.* Deliverable-or-stale is itself an up-set: once
///   stable, always stable. This does **not** follow from the other two ---
///   a gate with `deliverable(p) = (p == 0)` and `stale` always false
///   satisfies both and still returns the event to *waiting* once another
///   release advances progress, stranding it. `deliverable` alone need not
///   be monotone: causal contiguity is an equality, and it goes false on
///   overshoot. Terminal `stale` absorbs that overshoot for the shipped
///   gates. A gate whose `stale` does not fire there owes this law
///   separately.
///
/// These are laws an impl must satisfy, not properties the machine checks,
/// though [`check_gate_laws`] checks all three on a caller-supplied case.
///
/// A revisable gate, whose natural `stale` is not terminal, reports
/// `stale == false`. This works only where its `deliverable` is
/// independently up-closed, since stable up-closure then rests on
/// `deliverable` alone. A gate meeting neither needs its own machine rather
/// than a relaxed gate (`docs/metis-gate-stale-contract.adoc`).
///
/// The gate is handed the `sender` beside the dependency, because a bare
/// descriptor need not name which station authored the event. The machine
/// owns the stamp and the linearization and never asks the gate about
/// either.
pub trait Gate {
    /// The per-event dependency descriptor, carried as [`Event::deps`](crate::metis::Event::deps). Causal: a
    /// [`VersionVector`](crate::metis::VersionVector). Scalar [`Fifo`]: the sender's `u64`
    /// sequence number.
    type Dep;
    /// The progress state, ordered by information from bottom ([`Default`]); only its monotone
    /// rise under [`advance`](Self::advance) is load-bearing. Both shipped gates use a
    /// [`VersionVector`](crate::metis::VersionVector) (a join-semilattice; the scalar gate reads
    /// only the sender's own entry).
    type Progress: Default;

    /// Is an event from `sender` with `dep` releasable against `progress`? Need not be monotone
    /// *alone* (an equality rule is not), but `deliverable || stale` MUST be up-closed and the
    /// two MUST be disjoint; see the trait invariant.
    fn deliverable(progress: &Self::Progress, sender: u32, dep: &Self::Dep) -> bool;

    /// The delivery step: fold a released event into `progress`, monotonically *up* the
    /// information order.
    ///
    /// What it folds is the gate's choice: [`Causal`] folds the dependency vector, [`Fifo`] the
    /// sender's sequence number, a threshold gate the sender's identity alone (ignoring its
    /// `dep`). For the shipped [`VersionVector`](crate::metis::VersionVector) progresses this is a
    /// lattice join, but the machine relies only on the monotone rise, never on idempotence or a
    /// least upper bound.
    fn advance(progress: &mut Self::Progress, sender: u32, dep: &Self::Dep);

    /// Can an inserted event from `sender` with `dep` *never* become
    /// deliverable (a duplicate, or a replay already behind `progress`)? Such
    /// events are dropped at [`insert`](crate::metis::Ideal::insert) and
    /// reclaimed from a full backlog by the bounded
    /// [`try_insert`](crate::metis::Ideal::try_insert). MUST be *terminal*:
    /// up-closed in `progress` (once stale, stale for good) and disjoint from
    /// [`deliverable`](Self::deliverable), two of the three region laws of the
    /// trait invariant. Terminality lets the machine drop a stale event on the
    /// strength of the current `progress` alone. It never loses an event a
    /// later release would have delivered. Terminality is also how the shipped
    /// gates discharge the third law, stable up-closure, over the overshoot an
    /// equality `deliverable` leaves open.
    fn stale(progress: &Self::Progress, sender: u32, dep: &Self::Dep) -> bool;
}

/// A [`Gate`] whose progress changes only when [`Ideal`](crate::metis::Ideal)
/// releases an event.
///
/// This capability is required for product composition. [`And`] advances both
/// components after a product release, so neither component may require an
/// independent witness or another checked transition outside the delivery
/// machine. [`EpochGate`](crate::metis::EpochGate) deliberately does not
/// implement this trait: epoch adoption is separate authority exercised by
/// [`Ideal::adopt_epoch`](crate::metis::Ideal::adopt_epoch).
///
/// Implementors assert that every legal progress transition is induced by
/// [`Gate::advance`] for an event this gate admitted. The trait is an explicit
/// capability boundary; the machine cannot derive that property from the
/// three gate functions.
pub trait ReleaseDrivenGate: Gate {}