//! The grid's contract with untrusted bytes, written as an executable assertion.
//!
//! A normal public module rather than something behind a `fuzzing` feature,
//! because two callers need it and neither is the fuzzer: the committed
//! regression replay in `tests/regressions.rs` runs it on stable, and the
//! libFuzzer target in `fuzz/` runs it on nightly. A property asserted in one
//! and not the other is a property that drifts.
//!
//! ## Why this lives here and not in `shop-vt`
//!
//! `shop-vt` contains no `unsafe`. Fuzzing it with a no-op `Perform` asserts
//! only that it does not panic, which is the weakest thing a target can say and
//! reads as a defended path forever. The bytes reach real unchecked stores one
//! crate downstream: [`Grid::place_char`] writes through `get_unchecked_mut` on
//! the strength of invariants that the CSI cursor, DECSTBM, scroll and resize
//! paths maintain from those same bytes. So the parser is driven with the grid
//! as its `Perform`, and what is asserted is the preconditions of that store.
//!
//! ## The properties
//!
//! 1. **Structural invariants** ([`check_invariants`]) — the exact
//!    preconditions the `SAFETY` comment in `place_char` names, plus the ones
//!    the ring layout and history rest on. Checked after every chunk.
//! 2. **Row totality** — `row(r)` yields exactly `cols` cells for every visible
//!    row, which exercises the ring and region origin arithmetic rather than
//!    trusting it.
//! 3. **Wide pairs are whole** — a wide lead is never in the last column and is
//!    always followed by its spacer. This is what `heal_pair` is for, and a
//!    half-pair is how a renderer reads past the end of a row.
//! 4. **Damage is in range** — every row `take_damage` reports exists, and a
//!    second drain with no input in between reports nothing.
//! 5. **Resize keeps all of the above**, including a resize back to the
//!    original size, which is where `rewrap_history` runs.
//! 6. **The parser's buffers are bounded**, twice over: by the input, via
//!    [`MAX_RETAINED_PER_INPUT_BYTE`], and absolutely, via
//!    [`MAX_RETAINED_BYTES`]. The second is the one that catches an
//!    accumulator growing 1:1 with a stream nobody terminates, which the
//!    first cannot see.
//! 7. **Ground is always reachable** — after any byte sequence, `ESC \` then
//!    `ESC [ 0 m` returns the parser to Ground from every state. Cheap, and it
//!    catches a transition-table edit that strands a stream.

use crate::{CUR_ROW_INVALID, Grid};
use shop_vt::Parser;

/// Bytes the parser may hold per byte of input before the oracle calls it a
/// finding.
///
/// 4 is set from the worst case, which is a body buffer caught just past a
/// doubling: 2.0 bytes of capacity per byte pushed, plus the parameter list and
/// the OSC index table on top. The caps that hold it there are
/// `shop_vt::MAX_PARAMS`, `shop_vt::MAX_STRING_BYTES` and
/// `shop_vt::MAX_OSC_PARAMS`. Anything that pushes this back over 4 is either a
/// new accumulator or a cap that stopped being enforced.
pub const MAX_RETAINED_PER_INPUT_BYTE: usize = 4;

/// Slack for the buffers a fresh parser allocates up front (two 2 KiB bodies),
/// the parameter list's own spine, and the OSC field index table, which costs
/// 16 bytes per `;` and so amplifies hard against a stream of nothing else.
pub const RETAINED_BASE_BYTES: usize = 64 * 1024;

/// Bytes the parser may hold after any input at all, however long.
///
/// The ratio ceiling above cannot see an unterminated OSC or APC body: it
/// accumulates 1:1, so no per-input-byte limit above 1 fires, while the buffer
/// grows for as long as the writer keeps writing. This is the absolute bound
/// that catches that.
///
/// Set from the caps rather than guessed: one body buffer at
/// `shop_vt::MAX_STRING_BYTES`, the other resting at its initial 2 KiB, the OSC
/// index table at `shop_vt::MAX_OSC_PARAMS` doubled, and `shop_vt::MAX_PARAMS`
/// slots. That is about 8.42 MiB; 12 MiB leaves room for allocator rounding
/// without leaving room for an accumulator that does not stop.
pub const MAX_RETAINED_BYTES: usize = 12 * 1024 * 1024;

/// Panics if `grid` has broken anything `place_char`'s unchecked store rests on.
///
/// # Panics
///
/// By design. It is an oracle, and a panic is how it reports.
pub fn check_invariants(grid: &Grid) {
    let cols = grid.cols as usize;
    let rows = grid.rows as usize;
    assert!(cols >= 1 && rows >= 1, "grid collapsed to {cols}x{rows}");

    // 1. Both screens are exactly rows * cols. This is the bound the unchecked
    //    store is checked against and everything below assumes it.
    assert_eq!(grid.main.len(), cols * rows, "main is not rows * cols");
    assert_eq!(grid.alt.len(), cols * rows, "alt is not rows * cols");
    assert_eq!(grid.row_dirty.len(), rows, "row_dirty is not one per row");
    assert_eq!(
        grid.main_wrapped.len(),
        rows,
        "main_wrapped is not one per row"
    );
    assert_eq!(
        grid.alt_wrapped.len(),
        rows,
        "alt_wrapped is not one per row"
    );

    // 2. The cursor is on the screen. `place_char` clamps col on entry and
    //    relies on row having been kept in range by whoever moved it.
    assert!(
        (grid.cursor.row as usize) < rows,
        "cursor row {} outside {rows} rows",
        grid.cursor.row
    );
    assert!(
        (grid.cursor.col as usize) < cols,
        "cursor col {} outside {cols} cols",
        grid.cursor.col
    );

    // 3. The scroll region is a region, and it is inside the screen. DECSTBM
    //    takes both bounds from the parameter list, so this is untrusted input
    //    reaching the modulus in `phys_row`.
    assert!(
        grid.scroll_top <= grid.scroll_bottom,
        "scroll region inverted: {}..={}",
        grid.scroll_top,
        grid.scroll_bottom
    );
    assert!(
        (grid.scroll_bottom as usize) < rows,
        "scroll bottom {} outside {rows} rows",
        grid.scroll_bottom
    );

    // 4. Ring origins are rotations, not offsets into nothing.
    assert!(
        (grid.main_origin as usize) < rows,
        "main_origin out of range"
    );
    assert!((grid.alt_origin as usize) < rows, "alt_origin out of range");
    let region = (grid.scroll_bottom - grid.scroll_top + 1) as usize;
    assert!(
        (grid.region_origin as usize) < region,
        "region_origin {} outside a region of {region}",
        grid.region_origin
    );

    // 5. The cached row start is either invalid or a real row start. It is fed
    //    straight to the unchecked store as `start`.
    if grid.cur_row_start != CUR_ROW_INVALID {
        let start = grid.cur_row_start as usize;
        assert_eq!(start % cols, 0, "cur_row_start {start} is not a row start");
        assert!(
            start + cols <= grid.main.len(),
            "cur_row_start {start} leaves no row"
        );
    }

    // 6. History is bounded and every row of it is exactly the current width.
    //    `row()` hands these out as if they came off the live screen, so a
    //    short one is a short slice under every reader above it.
    assert!(
        grid.history.len() <= grid.history_limit,
        "history {} exceeds its limit {}",
        grid.history.len(),
        grid.history_limit
    );
    for (i, h) in grid.history.iter().enumerate() {
        assert_eq!(h.cells.len(), cols, "history row {i} is not {cols} wide");
    }
    assert!(
        grid.view_offset as usize <= grid.history.len(),
        "view_offset {} is past {} rows of history",
        grid.view_offset,
        grid.history.len()
    );
    if grid.on_alt {
        assert_eq!(grid.view_offset, 0, "alt screen holds a view offset");
    }

    // 7. Every visible row is a whole row, and every wide pair is whole. A lead
    //    in the last column, or a lead with no spacer after it, is a character
    //    claiming a column that is not there.
    for r in 0..grid.rows {
        let row = grid.row(r);
        assert_eq!(
            row.len(),
            cols,
            "row {r} is {} cells, not {cols}",
            row.len()
        );
        for (c, cell) in row.iter().enumerate() {
            if cell.is_wide() {
                assert!(c + 1 < cols, "wide lead in the last column of row {r}");
                assert!(
                    row[c + 1].is_spacer(),
                    "wide lead at {r},{c} has no spacer after it"
                );
            }
        }
    }
}

/// Panics if the damage report names a row that does not exist, or if a second
/// drain with no input in between still reports one.
///
/// # Panics
///
/// By design.
pub fn check_damage(grid: &mut Grid) {
    let d = grid.take_damage();
    for r in &d.dirty_rows {
        assert!(*r < grid.rows, "damage names row {r} of {} rows", grid.rows);
    }
    let again = grid.take_damage();
    assert!(
        again.dirty_rows.is_empty(),
        "damage repeated {} rows with no input between drains",
        again.dirty_rows.len()
    );
}

/// Feed `input` to a grid through the real parser and hold both to everything
/// above.
///
/// Returns the number of bytes that reached the parser, for the same reason
/// `git_command::oracle::check_line` returns a bool: without a return value
/// nothing can observe this function running at all, and `cargo mutants`
/// replacing the body with `()` would leave every test passing. A silently
/// empty oracle is the one failure this arrangement cannot afford.
///
/// # Panics
///
/// By design, on any violation.
pub fn check_bytes(input: &[u8]) -> usize {
    // The first two bytes choose the screen size, so one corpus covers the
    // one-column and one-row grids as well as ordinary ones. Everything after
    // them is the byte stream.
    let (cols, rows, stream) = match input {
        [c, r, rest @ ..] => (1 + u16::from(*c) % 200, 1 + u16::from(*r) % 60, rest),
        _ => (80, 24, input),
    };

    let mut grid = Grid::new(cols, rows);
    let mut parser = Parser::new();
    check_invariants(&grid);

    // Chunked rather than one call, because the parser's own state is what
    // survives a chunk boundary and a corpus of whole-sequence inputs would
    // never exercise a split one. Sixteen is small enough to land inside a
    // typical CSI.
    for chunk in stream.chunks(16) {
        parser.advance(&mut grid, chunk);
        check_invariants(&grid);
    }
    check_damage(&mut grid);
    check_invariants(&grid);

    // The amplification ceiling. See MAX_RETAINED_PER_INPUT_BYTE for why it is
    // set above today's behaviour rather than at it.
    let retained = parser.buffered_bytes();
    let ceiling = RETAINED_BASE_BYTES + stream.len().saturating_mul(MAX_RETAINED_PER_INPUT_BYTE);
    assert!(
        retained <= ceiling,
        "parser holds {retained} bytes after {} bytes of input, over the {ceiling} ceiling",
        stream.len()
    );
    assert!(
        retained <= MAX_RETAINED_BYTES,
        "parser holds {retained} bytes, over the {MAX_RETAINED_BYTES} absolute ceiling"
    );

    // Ground is reachable from every state these two sequences can leave the
    // parser in: `ESC \` closes any string state, and a complete CSI closes the
    // DCS passthrough that `\` opens from a DCS parameter state.
    parser.advance(&mut grid, b"\x1b\\");
    parser.advance(&mut grid, b"\x1b[0m");
    assert!(
        parser.in_ground(),
        "parser did not return to Ground after a terminator and a complete CSI"
    );
    check_invariants(&grid);

    // Resize is the other path into the unchecked store's preconditions, and
    // the only one that rewraps history. Sizes come from the input so the
    // corpus can steer them.
    let (nc, nr) = match stream {
        [a, b, ..] => (1 + u16::from(*a) % 200, 1 + u16::from(*b) % 60),
        _ => (1, 1),
    };
    grid.resize(nc, nr);
    check_invariants(&grid);
    grid.resize(cols, rows);
    check_invariants(&grid);
    check_damage(&mut grid);

    stream.len()
}