minerva 0.2.0

//! The pure decode core for the snapshot frame: the Creusot-provable half of
//! [`Rhapsody::from_snapshot_prefix`](crate::metis::Rhapsody), the rung's
//! second dual-homed core after the have-set's (`dot_set/wire/pure.rs`).
//!
//! Dual-homed: minerva compiles this file contract-free (`cfg(creusot)` is
//! never set by a normal build), while the detached `proofs/` crate includes
//! the same file by `#[path]` and proves it under `cargo creusot`. One
//! source, two readings; the proven code is the running code (R-18). The
//! subset discipline is the have-set core's, codified in
//! `proofs/README.adoc`; the choices that look odd below (index cursors,
//! unrolled big-endian sums, verdict enums instead of `?`, gated derives,
//! flat `Vec` output) are that discipline, not style.
//!
//! Proved: totality under `#[check(terminates)]` (termination, panic
//! freedom) and the run-shape bounds threaded between phases. Owed to
//! pearlite (R-25): the ascending merged order, the maximal-chain factoring
//! law, and rank-step canonicality, which this code validates and the
//! shaped suites plus the fuzz target pin.

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. 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 rhapsody *snapshot* wire encoding (PRD 0023): a
/// sibling codec to the canonical v2 rhapsody frame, in its own version
/// space (ruling R-8; the two frames evolve independently).
pub const SNAPSHOT_WIRE_V1: u8 = 0x01;
/// Frame header: one version byte, a `u32` big-endian chain-run count, then
/// a `u32` big-endian free-locus count.
pub const SNAPSHOT_WIRE_HEADER_LEN: usize = 9;
/// One chain-run header row, fixed width (the S189 layout decision:
/// fixed-width records, never varint rows): `[station: u32][base: u64]`
/// `[len: u32][anchor tag: u8][anchor station: u32][anchor index: u64]`
/// (zeroed for an origin anchor, so every row is one width) then the head
/// rank as a 17-byte stamp frame.
pub const SNAPSHOT_WIRE_RUN_HEADER_LEN: usize = 46;
/// One rank-step column record: a `u48` big-endian step (six bytes). Zero
/// is the clock fold's own successor; a positive value is the physical
/// advance with the logical reset to zero.
pub const SNAPSHOT_WIRE_STEP_LEN: usize = 6;
/// The 17-byte rank frame: one version byte plus the 16-byte big-endian
/// stamp payload. Mirrors `KAIROS_WIRE_LEN`; the layout equality is pinned
/// by test on the shipped side (the core is import-free by the dual-home
/// constraint).
pub const SNAPSHOT_RANK_FRAME_LEN: usize = 17;
/// The stamp frame's version byte this core accepts; pinned equal to the
/// `Kairos` codec's `KAIROS_WIRE_V1` by test on the shipped side.
pub const RANK_WIRE_V1: u8 = 0x01;
/// The anchor tag for a locus anchored at the origin, carrying zeroed
/// anchor-dot bytes in the fixed-width run row (and nothing in a free
/// record).
pub const ANCHOR_TAG_ORIGIN: u8 = 0x00;
/// The anchor tag for a locus in the region AFTER a dot.
pub const ANCHOR_TAG_AFTER: u8 = 0x01;
/// The anchor tag for a locus in the region BEFORE a dot.
pub const ANCHOR_TAG_BEFORE: u8 = 0x02;
/// The fixed prefix of one free-locus record before its variable anchor:
/// `[station: u32][index: u64][anchor tag: u8]`, the v2 locus-record shape.
pub const SNAPSHOT_WIRE_FREE_PREFIX_LEN: usize = 13;
/// The width of a free record's anchor dot when present.
pub const SNAPSHOT_WIRE_ANCHOR_LEN: usize = 12;
/// The smallest a free-locus record can be: the fixed prefix, an origin
/// anchor (tag only), and the 17-byte rank frame.
pub const SNAPSHOT_WIRE_FREE_MIN_LEN: usize =
    SNAPSHOT_WIRE_FREE_PREFIX_LEN + SNAPSHOT_RANK_FRAME_LEN;
/// The largest representable rank step: a `u48`'s ceiling. A physical
/// advance past this breaks the chain instead (the element rides as a free
/// locus or heads its own run).
pub const MAX_RANK_STEP: u64 = 0xFFFF_FFFF_FFFF;

/// The core's decode failure, variant-for-variant the public
/// `SnapshotDecodeError` without the `thiserror` derive (the S94 mask
/// lesson); the adapter maps it one-to-one, so the public error surface and
/// its `Display` text live on the shipped side.
#[cfg_attr(not(creusot), derive(Debug, Clone, Copy, PartialEq, Eq))]
pub enum PureSnapshotError {
    /// 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 run base or free-locus index carried the non-dot `0`.
    ZeroDot {
        /// The station of the offending zero-index dot.
        station: u32,
    },
    /// A chain run declared fewer than two elements (a one-element chain is
    /// a free locus; canonical form has exactly one spelling per value).
    RunTooShort {
        /// The station of the offending run.
        station: u32,
        /// The run's base dot index.
        base: u64,
    },
    /// A run's last dot (`base + len - 1`) exceeds [`u64::MAX`].
    RunOverflow {
        /// The station of the offending run.
        station: u32,
        /// The run's base dot index.
        base: u64,
        /// The run's declared element count (the four-byte field, widened).
        len: u64,
    },
    /// An anchor tag above `0x02` (only origin, after, before are known).
    BadAnchorTag {
        /// The unrecognized tag byte.
        tag: u8,
    },
    /// An origin-anchored run row carried non-zero anchor-dot padding
    /// (canonical form zeroes the unused fixed-width bytes).
    NonCanonicalOriginAnchor {
        /// The station of the offending run head.
        station: u32,
        /// The dot index of the offending run head.
        index: u64,
    },
    /// A rank frame's leading byte is not a stamp version this build
    /// understands.
    BadRankVersion(u8),
    /// A rank step would advance the physical component past [`u64::MAX`].
    RankOverflow {
        /// The station of the offending element.
        station: u32,
        /// The dot index of the offending element.
        index: u64,
    },
    /// A positive rank step decoded to exactly the successor rank (the
    /// rollover overlap); canonical form spells the successor as step zero.
    NonCanonicalRankStep {
        /// The station of the offending element.
        station: u32,
        /// The dot index of the offending element.
        index: u64,
    },
    /// The merged dot order (chain runs and free loci interleaved) was not
    /// strictly ascending: unsorted sections, overlapping runs, or a
    /// duplicated dot.
    NonAscendingLoci {
        /// The preceding dot's station.
        previous_station: u32,
        /// The preceding dot's index.
        previous_index: u64,
        /// The offending dot's station.
        found_station: u32,
        /// The offending dot's index.
        found_index: u64,
    },
    /// A dot-consecutive pair that satisfies the chain law was encoded
    /// split (across two runs, a run boundary and a free locus, or two free
    /// loci); canonical form factors maximal chains, so exactly one
    /// spelling exists per value.
    SplitChain {
        /// The station of the pair.
        station: u32,
        /// The dot index of the second element (the one that should have
        /// continued its predecessor's chain).
        index: u64,
    },
}

/// One decoded locus in flat form: the woven dot, its anchor (tag plus dot
/// fields, zeroed for the origin), and its rank unpacked into the four
/// stamp fields. The adapter reassembles `Locus { anchor, rank }` and folds
/// the map; the core stays map-free (the subset discipline).
#[cfg_attr(not(creusot), derive(Debug, Clone, Copy, PartialEq, Eq))]
pub struct PureLocus {
    /// The woven dot's station.
    pub station: u32,
    /// The woven dot's index (`>= 1`; the non-dot `0` is refused).
    pub index: u64,
    /// The anchor tag: origin, after, or before.
    pub anchor_tag: u8,
    /// The anchor dot's station (zero for an origin anchor).
    pub anchor_station: u32,
    /// The anchor dot's index (zero for an origin anchor).
    pub anchor_index: u64,
    /// The rank's physical component.
    pub physical: u64,
    /// The rank's logical component.
    pub logical: u16,
    /// The rank's kairotic component.
    pub kairotic: u16,
    /// The rank's minting station component.
    pub rank_station: u32,
}

/// One validated chain-run header row: the head locus plus the run's
/// declared element count (`>= 2`; the interior elements are materialized
/// from the rank-step column).
#[cfg_attr(not(creusot), derive(Debug, Clone, Copy, PartialEq, Eq))]
pub struct RunRow {
    /// The run's first element (the only one whose anchor is free-form).
    pub head: PureLocus,
    /// The run's element count, at least two (the four-byte field, widened
    /// at the read so the dot arithmetic stays cast-free).
    pub len: u64,
}

/// A structurally validated snapshot frame: the flat, map-free reading of
/// exactly the bytes a canonical encoder produces. `runs` carries every
/// chain-run element expanded in frame order (each run's elements
/// dot-consecutive, interior anchors implied AFTER the predecessor);
/// `free` carries the free loci in frame order; the merged dot order is
/// strictly ascending and maximal-chain factored (validated, not restated
/// here). The adapter folds both into the `BTreeMap` skeleton form.
#[cfg_attr(not(creusot), derive(Debug, Clone, PartialEq, Eq))]
pub struct PureSnapshot {
    /// Every chain-run element, expanded, in frame order.
    pub runs: Vec<PureLocus>,
    /// Every free locus, in frame order.
    pub free: Vec<PureLocus>,
    /// The number of frame bytes consumed (the prefix boundary, before the
    /// visible have-set suffix the adapter decodes).
    pub consumed: usize,
}

/// Big-endian `u16` at `bytes[at..at + 2]`, unrolled so every overflow
/// obligation is a constant bound.
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
#[cfg_attr(creusot, ::creusot_std::macros::requires(at@ + 2 <= bytes@.len()))]
const fn be_u16(bytes: &[u8], at: usize) -> u16 {
    (bytes[at] as u16) * 0x0100 + (bytes[at + 1] as u16)
}

/// Big-endian `u32` at `bytes[at..at + 4]`, unrolled as [`be_u16`] is.
#[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 `u32` at `bytes[at..at + 4]`, widened into a `u64` at the
/// read so no call site casts (the four-byte run-length field is compared
/// and added against `u64` dot arithmetic).
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
#[cfg_attr(creusot, ::creusot_std::macros::requires(at@ + 4 <= bytes@.len()))]
const fn be_u32_widened(bytes: &[u8], at: usize) -> u64 {
    (bytes[at] as u64) * 0x0100_0000
        + (bytes[at + 1] as u64) * 0x0001_0000
        + (bytes[at + 2] as u64) * 0x0000_0100
        + (bytes[at + 3] as u64)
}

/// Big-endian `u48` at `bytes[at..at + 6]` (a rank-step column record),
/// widened into a `u64` whose top sixteen bits are zero.
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
#[cfg_attr(creusot, ::creusot_std::macros::requires(at@ + 6 <= bytes@.len()))]
const fn be_u48(bytes: &[u8], at: usize) -> u64 {
    (bytes[at] as u64) * 0x0100_0000_0000
        + (bytes[at + 1] as u64) * 0x0001_0000_0000
        + (bytes[at + 2] as u64) * 0x0000_0100_0000
        + (bytes[at + 3] as u64) * 0x0000_0001_0000
        + (bytes[at + 4] as u64) * 0x0000_0000_0100
        + (bytes[at + 5] as u64)
}

/// Big-endian `u64` at `bytes[at..at + 8]`, unrolled as [`be_u16`] 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.
#[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
    }
}

/// The clock's send-step successor: logical bumps, rolling into the next
/// physical unit at the `u16::MAX` sentinel (the S86 fold fix). Duplicated
/// from `fold::advance` because the dual-home constraint forbids imports;
/// the Kani harness `snapshot_rank_step_matches_the_clock_fold` proves the
/// two equal over every pair, so drift decodes nothing the clock never
/// mints.
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
#[must_use]
pub const fn rank_successor(physical: u64, logical: u16) -> (u64, u16) {
    let bumped = logical.saturating_add(1);
    if bumped == u16::MAX {
        (physical.saturating_add(1), 0)
    } else {
        (physical, bumped)
    }
}

/// The chain law: whether `next` continues a chain from `prev`, the caller
/// having established dot adjacency (`next.index == prev.index + 1`, same
/// station). Shared verbatim by the encoder's greedy factoring and the
/// decoder's split-chain refusal; that sharing is what makes the factoring
/// canonical.
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
#[must_use]
pub const fn chainable(prev: &PureLocus, next: &PureLocus) -> bool {
    if next.anchor_tag != ANCHOR_TAG_AFTER {
        return false;
    }
    if next.anchor_station != prev.station {
        return false;
    }
    if next.anchor_index != prev.index {
        return false;
    }
    if next.kairotic != prev.kairotic {
        return false;
    }
    if next.rank_station != prev.rank_station {
        return false;
    }
    let (successor_physical, successor_logical) = rank_successor(prev.physical, prev.logical);
    if next.physical == successor_physical && next.logical == successor_logical {
        return true;
    }
    next.logical == 0
        && next.physical > prev.physical
        && next.physical - prev.physical <= MAX_RANK_STEP
}

/// One decode phase's verdict: the advanced cursor, or the frame's refusal.
/// A domain enum rather than `Result`, for the same dual-home reason as the
/// have-set core's `RunBlock`: the terminates reading cannot spec `?`'s
/// desugar, and the lint posture forbids the manual propagation match.
pub enum Cursor {
    /// The phase validated; the cursor past its section.
    Advanced(usize),
    /// The frame's refusal, verbatim.
    Refused(PureSnapshotError),
}

/// Decodes and validates the chain-run header table: `run_count` fixed-width
/// rows starting at `pos`, each pushed onto `rows`. Per row: the byte
/// budget, the non-zero base, the two-element minimum, the `u64` end, the
/// anchor tag and origin padding, and the rank frame's version.
#[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<i: Int> 0 <= i && i < (*rows)@.len() ==>
        (*rows)@[i].len@ >= 2
        && (*rows)@[i].head.index@ >= 1
        && (*rows)@[i].head.index@ + (*rows)@[i].len@ <= 18446744073709551616
))]
#[cfg_attr(creusot, ::creusot_std::macros::ensures(
    forall<i: Int> 0 <= i && i < (^rows)@.len() ==>
        (^rows)@[i].len@ >= 2
        && (^rows)@[i].head.index@ >= 1
        && (^rows)@[i].head.index@ + (^rows)@[i].len@ <= 18446744073709551616
))]
#[cfg_attr(creusot, ::creusot_std::macros::ensures(match result {
    Cursor::Advanced(new_pos) => new_pos@ <= bytes@.len(),
    Cursor::Refused(_) => true,
}))]
fn decode_rows(bytes: &[u8], pos: usize, run_count: u32, rows: &mut Vec<RunRow>) -> Cursor {
    let mut pos = pos;
    let mut r: u32 = 0;
    #[cfg_attr(creusot, variant(run_count@ - r@))]
    #[cfg_attr(creusot, invariant(pos@ <= bytes@.len()))]
    #[cfg_attr(creusot, invariant(
        forall<i: Int> 0 <= i && i < rows@.len() ==>
            rows@[i].len@ >= 2
            && rows@[i].head.index@ >= 1
            && rows@[i].head.index@ + rows@[i].len@ <= 18446744073709551616
    ))]
    while r < run_count {
        if bytes.len() - pos < SNAPSHOT_WIRE_RUN_HEADER_LEN {
            return Cursor::Refused(PureSnapshotError::UnexpectedLength {
                expected: expected_at(pos, SNAPSHOT_WIRE_RUN_HEADER_LEN),
                found: bytes.len(),
            });
        }
        let station = be_u32(bytes, pos);
        let base = be_u64(bytes, pos + 4);
        let len = be_u32_widened(bytes, pos + 12);
        let anchor_tag = bytes[pos + 16];
        let anchor_station = be_u32(bytes, pos + 17);
        let anchor_index = be_u64(bytes, pos + 21);
        let rank_version = bytes[pos + 29];
        let physical = be_u64(bytes, pos + 30);
        let logical = be_u16(bytes, pos + 38);
        let kairotic = be_u16(bytes, pos + 40);
        let rank_station = be_u32(bytes, pos + 42);
        pos += SNAPSHOT_WIRE_RUN_HEADER_LEN;

        if base == 0 {
            return Cursor::Refused(PureSnapshotError::ZeroDot { station });
        }
        if len < 2 {
            return Cursor::Refused(PureSnapshotError::RunTooShort { station, base });
        }
        // The run occupies `base ..= base + (len - 1)`; reject an end past
        // the `u64` ceiling rather than wrapping. `len >= 2` here, so the
        // subtraction is total.
        if len - 1 > u64::MAX - base {
            return Cursor::Refused(PureSnapshotError::RunOverflow { station, base, len });
        }
        if anchor_tag > ANCHOR_TAG_BEFORE {
            return Cursor::Refused(PureSnapshotError::BadAnchorTag { tag: anchor_tag });
        }
        // The fixed-width row zeroes the anchor dot for an origin head;
        // any other padding is a second spelling of the same value.
        if anchor_tag == ANCHOR_TAG_ORIGIN && (anchor_station != 0 || anchor_index != 0) {
            return Cursor::Refused(PureSnapshotError::NonCanonicalOriginAnchor {
                station,
                index: base,
            });
        }
        if rank_version != RANK_WIRE_V1 {
            return Cursor::Refused(PureSnapshotError::BadRankVersion(rank_version));
        }

        rows.push(RunRow {
            head: PureLocus {
                station,
                index: base,
                anchor_tag,
                anchor_station,
                anchor_index,
                physical,
                logical,
                kairotic,
                rank_station,
            },
            len,
        });
        r += 1;
    }
    Cursor::Advanced(pos)
}

/// Expands every run's rank-step column into its interior elements,
/// pushing head then interiors onto `out` in dot order. Each step is
/// validated as it is read: zero is the clock successor; a positive step
/// advances the physical (refused past the `u64` ceiling) and resets the
/// logical, refused where it collides with the successor spelling (the
/// rollover overlap), so every accepted rank has exactly one encoding.
#[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<i: Int> 0 <= i && i < rows@.len() ==>
        rows@[i].len@ >= 2
        && rows@[i].head.index@ >= 1
        && rows@[i].head.index@ + rows@[i].len@ <= 18446744073709551616
))]
#[cfg_attr(creusot, ::creusot_std::macros::ensures(match result {
    Cursor::Advanced(new_pos) => new_pos@ <= bytes@.len(),
    Cursor::Refused(_) => true,
}))]
fn decode_columns(bytes: &[u8], pos: usize, rows: &[RunRow], out: &mut Vec<PureLocus>) -> Cursor {
    let mut pos = pos;
    let mut ri: usize = 0;
    #[cfg_attr(creusot, variant(rows@.len() - ri@))]
    #[cfg_attr(creusot, invariant(pos@ <= bytes@.len()))]
    #[cfg_attr(creusot, invariant(ri@ <= rows@.len()))]
    while ri < rows.len() {
        let row = &rows[ri];
        let station = row.head.station;
        let base = row.head.index;
        out.push(PureLocus {
            station,
            index: base,
            anchor_tag: row.head.anchor_tag,
            anchor_station: row.head.anchor_station,
            anchor_index: row.head.anchor_index,
            physical: row.head.physical,
            logical: row.head.logical,
            kairotic: row.head.kairotic,
            rank_station: row.head.rank_station,
        });
        let mut previous_physical = row.head.physical;
        let mut previous_logical = row.head.logical;
        let len = row.len;
        let mut k: u64 = 1;
        #[cfg_attr(creusot, variant(len@ - k@))]
        #[cfg_attr(creusot, invariant(pos@ <= bytes@.len()))]
        #[cfg_attr(creusot, invariant(1 <= k@))]
        while k < len {
            if bytes.len() - pos < SNAPSHOT_WIRE_STEP_LEN {
                return Cursor::Refused(PureSnapshotError::UnexpectedLength {
                    expected: expected_at(pos, SNAPSHOT_WIRE_STEP_LEN),
                    found: bytes.len(),
                });
            }
            let step = be_u48(bytes, pos);
            pos += SNAPSHOT_WIRE_STEP_LEN;
            // The row check proved `base + (len - 1)` fits, and `k < len`,
            // so the element's dot is total arithmetic.
            let index = base + k;
            let (physical, logical) = if step == 0 {
                rank_successor(previous_physical, previous_logical)
            } else {
                if step > u64::MAX - previous_physical {
                    return Cursor::Refused(PureSnapshotError::RankOverflow { station, index });
                }
                let advanced = previous_physical + step;
                let (successor_physical, successor_logical) =
                    rank_successor(previous_physical, previous_logical);
                // The rollover overlap: a step of one from a logical at the
                // sentinel's edge spells the successor a second way.
                if advanced == successor_physical && successor_logical == 0 {
                    return Cursor::Refused(PureSnapshotError::NonCanonicalRankStep {
                        station,
                        index,
                    });
                }
                (advanced, 0)
            };
            out.push(PureLocus {
                station,
                index,
                anchor_tag: ANCHOR_TAG_AFTER,
                anchor_station: station,
                anchor_index: index - 1,
                physical,
                logical,
                kairotic: row.head.kairotic,
                rank_station: row.head.rank_station,
            });
            previous_physical = physical;
            previous_logical = logical;
            k += 1;
        }
        ri += 1;
    }
    Cursor::Advanced(pos)
}

/// Decodes and validates the free-locus section: `free_count` records in
/// the v2 locus-record shape (dot, tagged anchor, 17-byte rank frame),
/// pushed onto `out` in frame order.
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
#[cfg_attr(creusot, ::creusot_std::macros::requires(pos@ <= bytes@.len()))]
#[cfg_attr(creusot, ::creusot_std::macros::ensures(match result {
    Cursor::Advanced(new_pos) => new_pos@ <= bytes@.len(),
    Cursor::Refused(_) => true,
}))]
fn decode_free(bytes: &[u8], pos: usize, free_count: u32, out: &mut Vec<PureLocus>) -> Cursor {
    let mut pos = pos;
    let mut f: u32 = 0;
    #[cfg_attr(creusot, variant(free_count@ - f@))]
    #[cfg_attr(creusot, invariant(pos@ <= bytes@.len()))]
    while f < free_count {
        if bytes.len() - pos < SNAPSHOT_WIRE_FREE_PREFIX_LEN {
            return Cursor::Refused(PureSnapshotError::UnexpectedLength {
                expected: expected_at(pos, SNAPSHOT_WIRE_FREE_MIN_LEN),
                found: bytes.len(),
            });
        }
        let station = be_u32(bytes, pos);
        let index = be_u64(bytes, pos + 4);
        let anchor_tag = bytes[pos + 12];
        pos += SNAPSHOT_WIRE_FREE_PREFIX_LEN;
        if index == 0 {
            return Cursor::Refused(PureSnapshotError::ZeroDot { station });
        }
        let mut anchor_station: u32 = 0;
        let mut anchor_index: u64 = 0;
        if anchor_tag == ANCHOR_TAG_AFTER || anchor_tag == ANCHOR_TAG_BEFORE {
            if bytes.len() - pos < SNAPSHOT_WIRE_ANCHOR_LEN {
                return Cursor::Refused(PureSnapshotError::UnexpectedLength {
                    expected: expected_at(pos, SNAPSHOT_WIRE_ANCHOR_LEN + SNAPSHOT_RANK_FRAME_LEN),
                    found: bytes.len(),
                });
            }
            anchor_station = be_u32(bytes, pos);
            anchor_index = be_u64(bytes, pos + 4);
            pos += SNAPSHOT_WIRE_ANCHOR_LEN;
        } else if anchor_tag != ANCHOR_TAG_ORIGIN {
            return Cursor::Refused(PureSnapshotError::BadAnchorTag { tag: anchor_tag });
        }
        if bytes.len() - pos < SNAPSHOT_RANK_FRAME_LEN {
            return Cursor::Refused(PureSnapshotError::UnexpectedLength {
                expected: expected_at(pos, SNAPSHOT_RANK_FRAME_LEN),
                found: bytes.len(),
            });
        }
        let rank_version = bytes[pos];
        if rank_version != RANK_WIRE_V1 {
            return Cursor::Refused(PureSnapshotError::BadRankVersion(rank_version));
        }
        let physical = be_u64(bytes, pos + 1);
        let logical = be_u16(bytes, pos + 9);
        let kairotic = be_u16(bytes, pos + 11);
        let rank_station = be_u32(bytes, pos + 13);
        pos += SNAPSHOT_RANK_FRAME_LEN;

        out.push(PureLocus {
            station,
            index,
            anchor_tag,
            anchor_station,
            anchor_index,
            physical,
            logical,
            kairotic,
            rank_station,
        });
        f += 1;
    }
    Cursor::Advanced(pos)
}

/// Walks the merged dot order of the two sections (run elements in frame
/// order, free loci in frame order) and validates the two global canonical
/// laws the sections cannot state alone: the merged order is strictly
/// ascending (which also refuses overlapping runs and duplicated dots),
/// and no dot-consecutive pair that satisfies the chain law sits split
/// across a chain boundary (a free locus, or a run head, immediately after
/// its would-be predecessor), so the maximal-chain factoring is the
/// frame's only spelling. Returns `None` when the frame is canonical.
#[cfg_attr(creusot, ::creusot_std::macros::check(terminates))]
const fn check_merged_order(
    rows: &[RunRow],
    runs: &[PureLocus],
    free: &[PureLocus],
) -> Option<PureSnapshotError> {
    let mut run_cursor: usize = 0;
    let mut free_cursor: usize = 0;
    // Interior elements left in the current run; zero means the next pick
    // from the run stream begins a fresh row at its head.
    let mut remaining_in_row: u64 = 0;
    let mut row_index: usize = 0;
    let mut has_previous = false;
    let mut previous = PureLocus {
        station: 0,
        index: 0,
        anchor_tag: 0,
        anchor_station: 0,
        anchor_index: 0,
        physical: 0,
        logical: 0,
        kairotic: 0,
        rank_station: 0,
    };
    #[cfg_attr(creusot, variant((runs@.len() - run_cursor@) + (free@.len() - free_cursor@)))]
    #[cfg_attr(creusot, invariant(run_cursor@ <= runs@.len()))]
    #[cfg_attr(creusot, invariant(free_cursor@ <= free@.len()))]
    while run_cursor < runs.len() || free_cursor < free.len() {
        // Pick the smaller dot of the two stream heads; a tie is a
        // duplicate, refused by the strict-ascent check below.
        let take_run = if run_cursor >= runs.len() {
            false
        } else if free_cursor >= free.len() {
            true
        } else {
            let r = &runs[run_cursor];
            let f = &free[free_cursor];
            r.station < f.station || (r.station == f.station && r.index <= f.index)
        };
        // Whether the picked element begins a chain (a free locus, or a
        // run head): interior elements are chained to their predecessor by
        // construction and skip the split check.
        let begins_chain: bool;
        let current = if take_run {
            if remaining_in_row == 0 {
                // A fresh row: its head is being picked, and its interiors
                // (`len - 1`) queue behind it. The defensive bounds never
                // fire (the columns phase built `runs` from exactly these
                // rows, every `len` at least two), but keep the reads
                // total.
                if row_index < rows.len() {
                    let declared = rows[row_index].len;
                    remaining_in_row = if declared < 2 { 0 } else { declared - 1 };
                    row_index += 1;
                }
                begins_chain = true;
            } else {
                remaining_in_row -= 1;
                begins_chain = false;
            }
            let current = &runs[run_cursor];
            run_cursor += 1;
            current
        } else {
            begins_chain = true;
            let current = &free[free_cursor];
            free_cursor += 1;
            current
        };
        if has_previous {
            let ascending = previous.station < current.station
                || (previous.station == current.station && previous.index < current.index);
            if !ascending {
                return Some(PureSnapshotError::NonAscendingLoci {
                    previous_station: previous.station,
                    previous_index: previous.index,
                    found_station: current.station,
                    found_index: current.index,
                });
            }
            let consecutive = previous.station == current.station
                && previous.index < u64::MAX
                && current.index == previous.index + 1;
            if consecutive && begins_chain && chainable(&previous, current) {
                return Some(PureSnapshotError::SplitChain {
                    station: current.station,
                    index: current.index,
                });
            }
        }
        previous = PureLocus {
            station: current.station,
            index: current.index,
            anchor_tag: current.anchor_tag,
            anchor_station: current.anchor_station,
            anchor_index: current.anchor_index,
            physical: current.physical,
            logical: current.logical,
            kairotic: current.kairotic,
            rank_station: current.rank_station,
        };
        has_previous = true;
    }
    None
}

/// Decodes and structurally validates one snapshot frame's locus sections
/// from the start of `bytes`, returning the flat form and the consumed
/// length (the visible have-set suffix is the adapter's, decoded by the
/// have-set codec after this prefix). Check order: the header (length,
/// version), the run table (per row: length, non-zero base, two-element
/// minimum, `u64` end, anchor tag, origin padding, rank version), the
/// rank-step columns (per step: length, physical ceiling, the rollover
/// overlap), the free section (per record: length, non-zero dot, anchor
/// tag, rank version), then the merged order (strict ascent, split
/// chains).
///
/// Allocation is bounded by the input, never a declared count: every row,
/// step, and record is length-checked before it is read, and every
/// materialized element is backed by at least six frame bytes, so a frame
/// claiming `u32::MAX` of anything is refused against the buffer it cannot
/// fill (the PRD 0016 budget discipline; expansion is linear, roughly 7x).
///
/// # Errors
/// The [`PureSnapshotError`] 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(),
    Err(_) => true,
}))]
pub fn decode_prefix(bytes: &[u8]) -> Result<PureSnapshot, PureSnapshotError> {
    if bytes.len() < SNAPSHOT_WIRE_HEADER_LEN {
        return Err(PureSnapshotError::UnexpectedLength {
            expected: SNAPSHOT_WIRE_HEADER_LEN,
            found: bytes.len(),
        });
    }
    let version = bytes[0];
    if version != SNAPSHOT_WIRE_V1 {
        return Err(PureSnapshotError::UnknownVersion(version));
    }
    let run_count = be_u32(bytes, 1);
    let free_count = be_u32(bytes, 5);
    let pos = SNAPSHOT_WIRE_HEADER_LEN;

    let mut rows: Vec<RunRow> = Vec::new();
    let pos = match decode_rows(bytes, pos, run_count, &mut rows) {
        Cursor::Refused(error) => return Err(error),
        Cursor::Advanced(new_pos) => new_pos,
    };

    let mut runs: Vec<PureLocus> = Vec::new();
    let pos = match decode_columns(bytes, pos, &rows, &mut runs) {
        Cursor::Refused(error) => return Err(error),
        Cursor::Advanced(new_pos) => new_pos,
    };

    let mut free: Vec<PureLocus> = Vec::new();
    let pos = match decode_free(bytes, pos, free_count, &mut free) {
        Cursor::Refused(error) => return Err(error),
        Cursor::Advanced(new_pos) => new_pos,
    };

    if let Some(error) = check_merged_order(&rows, &runs, &free) {
        return Err(error);
    }
    Ok(PureSnapshot {
        runs,
        free,
        consumed: pos,
    })
}