minerva 0.2.0

//! The verified span substrate: a contiguous run of one station's dots (T1).
//!
//! A [`Span`] is the unit the have-set wire frame already speaks (a run of
//! consecutive dots, 16 bytes on the wire) and the shape the `StationDots`
//! floor and exception runs already are without naming it. Stating that unit
//! once, on a type whose every operation is heap-free scalar arithmetic over
//! fixed-width values, gives the run arithmetic that today lives inline in
//! `dot_set/wire.rs` and `StationDots::intersect` one audited home and, per
//! ruling R-9 as written, lets the span algebra be discharged *totally* by Kani
//! rather than sampled (the Kani harnesses in the sibling `proofs` module;
//! the proptest twins sit at the foot of this file, in the S86 idiom).
//!
//! This slice ships the substrate as `pub(crate)`: the public `Dot` rename
//! rides the 0.2.0 boundary (facade contract C11), and `Span` sits under the
//! existing `(u32, u64)` tuple surface until then. The type is deliberately
//! standalone this slice; wire and intersect adoption is deferred (see the
//! slice record), because retrofitting the two shipped sites would be a
//! rewrite carrying `station` into per-`StationDots` inner loops that do not
//! hold it, not the simplification the contract licenses, and byte identity on
//! the wire frame is protocol (ruling R-8). The substrate lands verified and
//! ready; its consumers arrive with C11.
//!
//! Because adoption is deferred, the algebra is exercised only by the
//! always-on property tests (the sampled twins of the Kani harnesses) and the
//! `cfg(kani)` proofs; the `dead_code` allow below records that the surface is
//! deliberately ahead of its in-tree caller, not orphaned. The `pub(crate)`
//! reach is the C11 target: every consumer sits inside `metis` today, so the
//! `redundant_pub_crate` allow marks intent, not accident.
#![allow(dead_code, clippy::redundant_pub_crate)]

use core::num::NonZeroU64;

#[cfg(kani)]
mod proofs;

/// A contiguous run `start..=end` of one station's dots.
///
/// A dot is `(station, seq)` with `seq >= 1` (the crate's 1-based convention;
/// `0` is not a dot), so both bounds are [`NonZeroU64`] and the zero-dot hazard
/// is unconstructible. The invariant `start <= end` is enforced at every
/// constructor, so a `Span` names a non-empty run and [`len`](Self::len) is at
/// least one. Field-swap (mixing a station with another's dot) is out of scope
/// by construction: a span carries exactly one `station`.
///
/// # The normal form the crate already is
///
/// A per-station canonical span list (sorted, disjoint, non-abutting) is the
/// form the have-set wire frame and the `StationDots` floor-plus-exceptions
/// representation both already hold; [`coalesce`](Self::coalesce) is the fold
/// that maintains it and [`split_at`](Self::split_at) its inverse. The algebra
/// is a partial commutative monoid per station: coalesce is commutative, and
/// associative where every intermediate pair is defined.
///
/// # Totality
///
/// Every operation is total and panic-free. [`len`](Self::len) computes in
/// [`u64`] and cannot overflow below the ceiling (mirroring the wire codec's
/// compute-in-`u64` discipline); the run's own bounds already fit `u64`, so its
/// cardinality does too.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub(crate) struct Span {
    /// The station whose dots this run names.
    pub(crate) station: u32,
    /// The first dot of the run (inclusive).
    pub(crate) start: NonZeroU64,
    /// The last dot of the run (inclusive); `start <= end` by invariant.
    pub(crate) end: NonZeroU64,
}

impl Span {
    /// Builds a run `start..=end` on `station`, or `None` when `start > end`
    /// (the empty run a span never represents).
    ///
    /// The single honest constructor: it is the only way to mint a `Span`, so
    /// the `start <= end` invariant every method relies on holds for every
    /// value that exists.
    pub(crate) fn new(station: u32, start: NonZeroU64, end: NonZeroU64) -> Option<Self> {
        (start <= end).then_some(Self {
            station,
            start,
            end,
        })
    }

    /// Whether `dot` on `station` lies inside the run.
    ///
    /// Agrees with the range arithmetic `station == self.station && start <=
    /// dot <= end` (the Kani `contains_agrees_with_range` harness); a dot on
    /// another station is never contained.
    pub(crate) const fn contains(&self, station: u32, dot: NonZeroU64) -> bool {
        station == self.station && self.start.get() <= dot.get() && dot.get() <= self.end.get()
    }

    /// Whether `other` sits immediately after this run on the same station:
    /// `self.end + 1 == other.start`.
    ///
    /// The one-directional adjacency test coalesce reads: two abutting runs
    /// merge into one, which is exactly the maximality the wire frame's runs
    /// demand. Saturating at the ceiling closes the door on a run whose end is
    /// [`u64::MAX`] (nothing abuts it from above).
    pub(crate) const fn abuts(&self, other: &Self) -> bool {
        self.station == other.station && self.end.get().saturating_add(1) == other.start.get()
    }

    /// Coalesces two runs into their union when they overlap or abut, or hands
    /// both back unchanged when they are disjoint and separated (or on
    /// different stations).
    ///
    /// The partial monoid's operation: `Ok` is the merged run
    /// `min(start)..=max(end)`, `Err((self, other))` the two inputs returned so
    /// no information is lost on a non-merge. Commutative
    /// (`a.coalesce(b)` and `b.coalesce(a)` name the same union) and
    /// associative where every pair is defined; the Kani harnesses discharge
    /// both.
    ///
    /// # Errors
    ///
    /// Returns `Err((self, other))` when the runs neither overlap nor abut, so
    /// the caller keeps both spans.
    pub(crate) fn coalesce(self, other: Self) -> Result<Self, (Self, Self)> {
        if self.station != other.station {
            return Err((self, other));
        }
        // Overlap or abut, in either order: the runs merge iff neither lies
        // strictly beyond the other's end-plus-one. Computed in `u64` with a
        // saturating step so a run ending at the ceiling cannot overflow the
        // adjacency probe (the wire code's discipline).
        let mergeable = self.start.get() <= other.end.get().saturating_add(1)
            && other.start.get() <= self.end.get().saturating_add(1);
        if !mergeable {
            return Err((self, other));
        }
        let start = self.start.min(other.start);
        let end = self.end.max(other.end);
        Ok(Self {
            station: self.station,
            start,
            end,
        })
    }

    /// Splits the run at `seq` into the head `start..=seq-1` and the tail
    /// `seq..=end`.
    ///
    /// The inverse of [`coalesce`](Self::coalesce): when the cut lands strictly
    /// inside the run (`start < seq <= end`) the two abutting pieces coalesce
    /// back to the original (the Kani `split_then_coalesce_is_identity`
    /// harness). A `seq` outside that window does not split: the whole run comes
    /// back as the head with a `None` tail (a span is never empty, so a cut at
    /// or below `start`, or above `end`, leaves nothing to peel off). Returns
    /// `(head, tail)`.
    pub(crate) fn split_at(self, seq: NonZeroU64) -> (Self, Option<Self>) {
        // A genuine split needs a dot on each side: `start < seq <= end`. Below
        // or at `start` the tail would be the whole run and the head empty;
        // above `end` the head would be the whole run and the tail empty.
        // Neither is a span, so both degenerate to "no split".
        if seq <= self.start || seq > self.end {
            return (self, None);
        }
        // `seq > start >= 1`, so `seq - 1 >= 1` is a valid dot; the head is
        // `start..=seq-1` and the tail `seq..=end`, abutting at the cut.
        let head_end = NonZeroU64::new(seq.get() - 1).unwrap_or(self.start);
        let head = Self {
            station: self.station,
            start: self.start,
            end: head_end,
        };
        let tail = Self {
            station: self.station,
            start: seq,
            end: self.end,
        };
        (head, Some(tail))
    }

    /// The number of dots in the run: `end - start + 1`.
    ///
    /// At least one (a span is never empty) and computed in [`u64`], which
    /// cannot overflow below the ceiling because `end - start < end <= u64::MAX`
    /// (the Kani `len_never_overflows` harness discharges it totally).
    pub(crate) const fn len(&self) -> u64 {
        // `start <= end` by invariant, so the subtraction never underflows, and
        // `end - start` is strictly below `end`, so the `+ 1` cannot overflow.
        (self.end.get() - self.start.get()) + 1
    }
}

#[cfg(test)]
mod tests {
    //! The always-on sampled twins of the Kani span harnesses (the
    //! assurance-ladder rule: a proven law keeps its property-test gate).

    use super::Span;
    use core::num::NonZeroU64;
    use proptest::prelude::*;

    /// A valid span on `station`: `start <= end`, both non-zero.
    fn arb_span(station: u32) -> impl Strategy<Value = Span> {
        (1u64..=40, 1u64..=40).prop_map(move |(a, b)| {
            let (lo, hi) = (a.min(b), a.max(b));
            Span {
                station,
                start: NonZeroU64::new(lo).unwrap(),
                end: NonZeroU64::new(hi).unwrap(),
            }
        })
    }

    /// A dot in a range that overlaps the span domain, so containment is
    /// exercised on both sides of the bounds.
    fn arb_dot() -> impl Strategy<Value = NonZeroU64> {
        (1u64..=45).prop_map(|d| NonZeroU64::new(d).unwrap())
    }

    proptest! {
        /// `contains` agrees with the range arithmetic on the span's station,
        /// and is never true across stations.
        #[test]
        fn contains_agrees_with_range(span in arb_span(0), dot in arb_dot()) {
            let by_arith = span.start <= dot && dot <= span.end;
            prop_assert_eq!(span.contains(0, dot), by_arith);
            prop_assert!(!span.contains(1, dot));
        }

        /// `len` is `end - start + 1` and at least one.
        #[test]
        fn len_is_run_cardinality(span in arb_span(0)) {
            prop_assert_eq!(span.len(), span.end.get() - span.start.get() + 1);
            prop_assert!(span.len() >= 1);
        }

        /// `coalesce` is commutative on one station: either order yields the
        /// same union or the same symmetric non-merge.
        #[test]
        fn coalesce_is_commutative(a in arb_span(0), b in arb_span(0)) {
            match (a.coalesce(b), b.coalesce(a)) {
                (Ok(ab), Ok(ba)) => prop_assert_eq!(ab, ba),
                (Err((a1, b1)), Err((b2, a2))) => {
                    prop_assert_eq!(a1, a2);
                    prop_assert_eq!(b1, b2);
                }
                _ => prop_assert!(false, "coalesce disagrees on mergeability across argument order"),
            }
        }

        /// `coalesce` is associative where both groupings are defined.
        #[test]
        fn coalesce_is_associative_where_defined(
            a in arb_span(0), b in arb_span(0), c in arb_span(0),
        ) {
            if let (Ok(ab), Ok(bc)) = (a.coalesce(b), b.coalesce(c))
                && let (Ok(left), Ok(right)) = (ab.coalesce(c), a.coalesce(bc))
            {
                prop_assert_eq!(left, right);
            }
        }

        /// `split_at` then `coalesce` recovers the original span, and a no-op
        /// split returns the whole run unchanged.
        #[test]
        fn split_then_coalesce_is_identity(span in arb_span(0), seq in arb_dot()) {
            let (head, tail) = span.split_at(seq);
            if let Some(tail) = tail {
                prop_assert!(head.abuts(&tail));
                prop_assert_eq!(head.coalesce(tail), Ok(span));
            } else {
                prop_assert_eq!(head, span);
            }
        }

        /// Coalesce and abut agree with the wire codec's run maximality: two
        /// spans that abut coalesce, and their union spans both.
        #[test]
        fn abutting_spans_coalesce(a in arb_span(0), b in arb_span(0)) {
            if a.abuts(&b) {
                let merged = a.coalesce(b).expect("abutting spans merge");
                prop_assert_eq!(merged.start, a.start);
                prop_assert_eq!(merged.end, b.end);
            }
        }
    }
}