minerva 0.2.0

//! The pure decode core for the have-set frame: the Creusot-provable half of
//! [`DotSet::from_prefix`](crate::metis::DotSet::from_prefix), extracted under
//! the never-in-place discipline (horizons axis 5, S94; landed by ruling
//! R-18).
//!
//! This file is *dual-homed*: minerva compiles it contract-free (every proof
//! attribute is `#[cfg_attr(creusot, ...)]`, and `cfg(creusot)` is never set
//! by a normal build, so no proof dependency exists), and the detached
//! `proofs/` crate includes the same file by `#[path]` and compiles it under
//! `cargo creusot`, where the contracts come alive and the verification
//! conditions are discharged. One source, two readings; the shipped adapter
//! in `wire/mod.rs` is a thin fold over this core's output, so the proven
//! code is the running code, never a shadow.
//!
//! The subset discipline (the S94 record, so the proof tail does not wag the
//! production dog *twice*): index-cursor reads instead of slice patterns
//! (array destructuring ICEs the 0.12 translator), unrolled big-endian
//! assembly instead of shift loops (constant-bounded overflow obligations),
//! hand-rolled comparison guards instead of `checked_*` (no library specs
//! needed), a plain error enum (no `thiserror` mask), derives gated off
//! under `cfg(creusot)` (a derived `Eq` pulls a `DeepModel` obligation), and
//! flat `Vec` output (no map model; the `BTreeMap`/`BTreeSet` fold stays on
//! the shipped side of the adapter).
//!
//! What the contracts state: *totality* (no reachable panic on any input:
//! every index, subtraction, and addition discharges its VC) and the
//! *acceptance shape* (consumed never exceeds the input; stations strictly
//! ascending; every run non-empty). The remaining canonical-form
//! postconditions (same-station run separation, the no-empty-station
//! cross-condition, and the full decode/encode bijection) are recorded as
//! owed in the R-18 ruling; the shaped property tests keep pinning them.

extern crate alloc;

use alloc::vec::Vec;

/// The pearlite vocabulary (`Int` in the quantifiers) and the loop-spec
/// macros, alive only under the proofs crate's `cargo creusot` compile; a
/// normal minerva build strips these imports with the rest of the proof
/// reading. Loop-spec attributes must be bare idents (the desugaring pass
/// collects sibling `#[invariant]`/`#[variant]` attributes by single ident
/// only, and one collected pass keeps the variant closure in the
/// first-statement slot the termination checker reads); only the FIRST
/// loop-spec attribute on a loop expands as a macro and so needs importing,
/// here `variant`, which leads every loop. The trailing `invariant`s are
/// consumed as inert tokens by that same pass.
#[cfg(creusot)]
use ::creusot_std::macros::variant;
#[cfg(creusot)]
use ::creusot_std::prelude::Int;

/// Version tag for the canonical have-set wire encoding (PRD 0016).
pub const HAVE_SET_WIRE_V1: u8 = 0x01;
/// Frame header: one version byte plus a `u32` big-endian station count.
pub const HAVE_SET_WIRE_HEADER_LEN: usize = 5;
/// One station header: `u32` station, `u64` floor, `u32` run count.
pub const HAVE_SET_WIRE_STATION_HEADER_LEN: usize = 16;
/// One run: a `u64` big-endian `start` then a `u64` big-endian `len`.
pub const HAVE_SET_WIRE_RUN_LEN: usize = 16;

/// The core's decode failure, variant-for-variant the public
/// [`HaveSetDecodeError`](super::HaveSetDecodeError) without the `thiserror`
/// derive (the S94 mask lesson); the adapter maps it one-to-one, so the
/// public error surface and its `Display` text are untouched.
#[cfg_attr(not(creusot), derive(Debug, Clone, Copy, PartialEq, Eq))]
pub enum PureDecodeError {
    /// The leading version byte is not a version this build understands.
    UnknownVersion(u8),
    /// The input is shorter than a declared count requires.
    UnexpectedLength {
        /// A lower bound on the frame length the declared counts require.
        expected: usize,
        /// The actual length of the supplied input.
        found: usize,
    },
    /// A station entry carried `floor == 0` and no runs (canonical form
    /// holds an empty station absent).
    EmptyStation {
        /// The station whose entry was empty.
        station: u32,
    },
    /// Station entries were not strictly ascending.
    NonAscendingStations {
        /// The preceding entry's station id.
        previous: u32,
        /// The offending station id.
        found: u32,
    },
    /// A run declared a length of zero.
    ZeroLengthRun {
        /// The station whose run carried the illegal zero length.
        station: u32,
    },
    /// A run began at or below its absorption point (non-maximal form).
    NonMaximalRun {
        /// The station whose run was absorbable.
        station: u32,
        /// The offending run's start dot.
        start: u64,
    },
    /// A run's end (`start + len - 1`) exceeds [`u64::MAX`].
    RunOverflow {
        /// The station whose run overflowed.
        station: u32,
        /// The run's start dot.
        start: u64,
        /// The run's declared length.
        len: u64,
    },
    /// The frame's runs would materialize more dots than the input length
    /// justifies (the decompression-bomb budget).
    RunTooLong {
        /// The station whose run overran the budget.
        station: u32,
        /// The run's start dot.
        start: u64,
        /// The run's declared length.
        len: u64,
    },
}

/// A structurally validated frame: the flat, map-free reading of exactly the
/// bytes a canonical encoder produces. `stations` carries `(station, floor)`
/// in frame order; `runs` carries `(station, start, len)` in frame order,
/// each run's station equal to some station entry's and the runs of one
/// station contiguous. The adapter folds this into the `BTreeMap` form.
#[cfg_attr(not(creusot), derive(Debug, Clone, PartialEq, Eq))]
pub struct PureDecoded {
    /// Per frame station record, `(station, floor)`, strictly ascending.
    pub stations: Vec<(u32, u64)>,
    /// Every validated run, `(station, start, len)`, `len >= 1`, budget
    /// charged; grouped contiguously by station in frame order.
    pub runs: Vec<(u32, u64, u64)>,
    /// The number of frame bytes consumed (the prefix boundary).
    pub consumed: usize,
}

/// Big-endian `u32` at `bytes[at..at + 4]`. Unrolled so every overflow
/// obligation is a constant bound (each term is at most `255 << 24` and the
/// sum is at most `u32::MAX` exactly).
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
#[cfg_attr(creusot, ::creusot_std::macros::requires(at@ + 4 <= bytes@.len()))]
const fn be_u32(bytes: &[u8], at: usize) -> u32 {
    (bytes[at] as u32) * 0x0100_0000
        + (bytes[at + 1] as u32) * 0x0001_0000
        + (bytes[at + 2] as u32) * 0x0000_0100
        + (bytes[at + 3] as u32)
}

/// Big-endian `u64` at `bytes[at..at + 8]`, unrolled as [`be_u32`] is.
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
#[cfg_attr(creusot, ::creusot_std::macros::requires(at@ + 8 <= bytes@.len()))]
const fn be_u64(bytes: &[u8], at: usize) -> u64 {
    (bytes[at] as u64) * 0x0100_0000_0000_0000
        + (bytes[at + 1] as u64) * 0x0001_0000_0000_0000
        + (bytes[at + 2] as u64) * 0x0000_0100_0000_0000
        + (bytes[at + 3] as u64) * 0x0000_0001_0000_0000
        + (bytes[at + 4] as u64) * 0x0000_0000_0100_0000
        + (bytes[at + 5] as u64) * 0x0000_0000_0001_0000
        + (bytes[at + 6] as u64) * 0x0000_0000_0000_0100
        + (bytes[at + 7] as u64)
}

/// The error's `expected` field: the bytes the frame would need for the next
/// fixed-width record, saturating at the type ceiling so the arithmetic is
/// total without a slice-length axiom (unreachable in practice: a slice is
/// at most `isize::MAX` bytes).
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
const fn expected_at(pos: usize, need: usize) -> usize {
    if pos > usize::MAX - need {
        usize::MAX
    } else {
        pos + need
    }
}

/// One station's run-block verdict: the advanced cursor and remaining dot
/// budget, or the frame's refusal. A domain enum rather than `Result`,
/// deliberately: the terminates reading cannot spec `?`'s `Try::branch`
/// desugar (no termination contract upstream yet), and the crate's
/// `question_mark` lint forbids the manual propagation match over a
/// `Result`, so a `Result` here cannot satisfy both homes of this file at
/// once. The verdict enum says the same thing and both readers accept it
/// (the dual-home constraint, recorded in ruling R-18).
pub enum RunBlock {
    /// Every run validated: the cursor past the run block, and what remains
    /// of the whole-frame dot budget.
    Advanced(usize, u64),
    /// A run failed validation; the frame's refusal, verbatim.
    Refused(PureDecodeError),
}

/// Decodes and validates one station's `run_count` runs starting at `pos`,
/// pushing each `(station, start, len)` onto `runs` and returning the new
/// cursor and the remaining dot budget as a [`RunBlock`] verdict. Check
/// order per run is the shipped contract's: length, non-zero, budget,
/// maximality bound, `u64` end.
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
#[cfg_attr(creusot, ::creusot_std::macros::requires(pos@ <= bytes@.len()))]
#[cfg_attr(creusot, ::creusot_std::macros::requires(
    forall<k: Int> 0 <= k && k < (*runs)@.len() ==> (*runs)@[k].2@ >= 1
))]
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<k: Int> 0 <= k && k < (^runs)@.len() ==> (^runs)@[k].2@ >= 1
))]
#[cfg_attr(creusot, ::creusot_std::macros::ensures(match result {
    RunBlock::Advanced(new_pos, _) => new_pos@ <= bytes@.len(),
    RunBlock::Refused(_) => true,
}))]
fn decode_station_runs(
    bytes: &[u8],
    pos: usize,
    station: u32,
    floor: u64,
    run_count: u32,
    dot_budget: u64,
    runs: &mut Vec<(u32, u64, u64)>,
) -> RunBlock {
    let mut pos = pos;
    let mut dot_budget = dot_budget;
    // The lowest a run may start at and stay non-absorbable: strictly above
    // `floor + 1`, tracked forward as `previous end + 2`. `None` means the
    // ceiling closed the door on any further canonical run.
    let mut min_start: Option<u64> = if floor > u64::MAX - 2 {
        None
    } else {
        Some(floor + 2)
    };

    let mut r: u32 = 0;
    #[cfg_attr(creusot, variant(run_count@ - r@))]
    #[cfg_attr(creusot, invariant(pos@ <= bytes@.len()))]
    #[cfg_attr(creusot, invariant(
        forall<k: Int> 0 <= k && k < runs@.len() ==> runs@[k].2@ >= 1
    ))]
    while r < run_count {
        if bytes.len() - pos < HAVE_SET_WIRE_RUN_LEN {
            return RunBlock::Refused(PureDecodeError::UnexpectedLength {
                expected: expected_at(pos, HAVE_SET_WIRE_RUN_LEN),
                found: bytes.len(),
            });
        }
        let start = be_u64(bytes, pos);
        let len = be_u64(bytes, pos + 8);
        pos += HAVE_SET_WIRE_RUN_LEN;

        if len == 0 {
            return RunBlock::Refused(PureDecodeError::ZeroLengthRun { station });
        }
        // Charge the run's expansion against the whole-frame dot budget
        // before admitting a single dot.
        if len > dot_budget {
            return RunBlock::Refused(PureDecodeError::RunTooLong {
                station,
                start,
                len,
            });
        }
        dot_budget -= len;
        // Maximality and strict ascent share one bound (the shipped rustdoc):
        // a start below it would be absorbed into the floor or the previous
        // run, so the form is not canonical.
        match min_start {
            Some(bound) if start >= bound => {}
            _ => {
                return RunBlock::Refused(PureDecodeError::NonMaximalRun { station, start });
            }
        }
        // The run occupies `start ..= start + (len - 1)`; reject an end past
        // the `u64` ceiling rather than wrapping. `len >= 1` here, so the
        // subtraction is total.
        if len - 1 > u64::MAX - start {
            return RunBlock::Refused(PureDecodeError::RunOverflow {
                station,
                start,
                len,
            });
        }
        let last = start + (len - 1);
        // The next run must clear this end by at least two, or the two runs
        // would themselves absorb into one.
        min_start = if last > u64::MAX - 2 {
            None
        } else {
            Some(last + 2)
        };

        runs.push((station, start, len));
        r += 1;
    }
    RunBlock::Advanced(pos, dot_budget)
}

/// Decodes and structurally validates one canonical frame from the start of
/// `bytes`, returning the flat form and the consumed length. Exactly the
/// acceptance set and error assignment of the shipped
/// [`DotSet::from_prefix`](crate::metis::DotSet::from_prefix), whose
/// standalone budget is the input byte length (PRD 0016's
/// decompression-bomb rule, applied at the adapter): version, then per
/// station (length check, strict ascent, non-emptiness), then per run
/// (length check, non-zero length, dot budget, maximality bound, `u64`
/// end), in that order, so every input maps to the same verdict.
///
/// The run expansion may materialize at most `dot_budget` dots. An
/// embedding codec whose own validated structure bounds the honest set
/// passes that bound instead of the byte length (the rhapsody codecs pass
/// their decoded skeleton's cardinality, since visibility is a subset of
/// the skeleton); that also makes a *prefix* decode's acceptance
/// independent of whatever trails the frame (the S197 gate review's
/// finding: a byte-length budget read through an outer tail inflates with
/// the tail).
///
/// # Errors
/// The [`PureDecodeError`] variants, each mapped one-to-one onto the public
/// error by the adapter.
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
#[cfg_attr(creusot, ::creusot_std::macros::ensures(match result {
    Ok(d) => d.consumed@ <= bytes@.len()
        && (forall<i: Int, j: Int> 0 <= i && i < j && j < d.stations@.len()
            ==> d.stations@[i].0@ < d.stations@[j].0@)
        && (forall<k: Int> 0 <= k && k < d.runs@.len() ==> d.runs@[k].2@ >= 1),
    Err(_) => true,
}))]
pub fn decode_prefix_with_budget(
    bytes: &[u8],
    dot_budget: u64,
) -> Result<PureDecoded, PureDecodeError> {
    if bytes.len() < HAVE_SET_WIRE_HEADER_LEN {
        return Err(PureDecodeError::UnexpectedLength {
            expected: HAVE_SET_WIRE_HEADER_LEN,
            found: bytes.len(),
        });
    }
    let version = bytes[0];
    if version != HAVE_SET_WIRE_V1 {
        return Err(PureDecodeError::UnknownVersion(version));
    }
    let station_count = be_u32(bytes, 1);

    let mut pos = HAVE_SET_WIRE_HEADER_LEN;
    let mut stations: Vec<(u32, u64)> = Vec::new();
    let mut runs: Vec<(u32, u64, u64)> = Vec::new();
    let mut previous_station: Option<u32> = None;
    // The run expansion may materialize at most `dot_budget` dots (the
    // decompression-bomb budget; the standalone default is the input byte
    // length, PRD 0016).
    let mut dot_budget = dot_budget;

    let mut s: u32 = 0;
    #[cfg_attr(creusot, variant(station_count@ - s@))]
    #[cfg_attr(creusot, invariant(pos@ <= bytes@.len()))]
    #[cfg_attr(creusot, invariant(
        forall<i: Int, j: Int> 0 <= i && i < j && j < stations@.len()
            ==> stations@[i].0@ < stations@[j].0@
    ))]
    #[cfg_attr(creusot, invariant(match previous_station {
        Some(previous) => forall<i: Int> 0 <= i && i < stations@.len()
            ==> stations@[i].0@ <= previous@,
        None => stations@.len() == 0,
    }))]
    #[cfg_attr(creusot, invariant(
        forall<k: Int> 0 <= k && k < runs@.len() ==> runs@[k].2@ >= 1
    ))]
    while s < station_count {
        if bytes.len() - pos < HAVE_SET_WIRE_STATION_HEADER_LEN {
            return Err(PureDecodeError::UnexpectedLength {
                expected: expected_at(pos, HAVE_SET_WIRE_STATION_HEADER_LEN),
                found: bytes.len(),
            });
        }
        let station = be_u32(bytes, pos);
        let floor = be_u64(bytes, pos + 4);
        let run_count = be_u32(bytes, pos + 12);
        pos += HAVE_SET_WIRE_STATION_HEADER_LEN;

        if let Some(previous) = previous_station
            && station <= previous
        {
            return Err(PureDecodeError::NonAscendingStations {
                previous,
                found: station,
            });
        }
        previous_station = Some(station);

        if floor == 0 && run_count == 0 {
            // Canonical form holds an empty station absent; no encoder emits one.
            return Err(PureDecodeError::EmptyStation { station });
        }

        stations.push((station, floor));

        match decode_station_runs(bytes, pos, station, floor, run_count, dot_budget, &mut runs) {
            RunBlock::Refused(error) => return Err(error),
            RunBlock::Advanced(new_pos, new_budget) => {
                pos = new_pos;
                dot_budget = new_budget;
            }
        }
        s += 1;
    }

    Ok(PureDecoded {
        stations,
        runs,
        consumed: pos,
    })
}