varta-vlp 0.2.0

//! Kani symbolic-verification harnesses for [`crate::Frame`] and
//! [`crate::crc32c`].
//!
//! This module is gated `#[cfg(kani)]` so the harnesses are invisible to
//! every normal `cargo build` / `cargo test` invocation.  The Kani crate
//! is injected by `cargo kani` at proof time — there is no entry in
//! [`Cargo.toml`] for it, and the zero-registry-dependency invariant
//! documented in `CLAUDE.md` is preserved by construction.
//!
//! Run locally with `cargo kani -p varta-vlp`.  In CI, the
//! `kani-proofs` job in `.github/workflows/ci.yml` runs the same
//! command and is a required gate on every PR that touches
//! `crates/varta-vlp/**`.
//!
//! ### Split-harness design
//!
//! Combining the CRC-table loop (28 iterations × 256-entry lookup) with
//! the full decode path explodes CBMC's state space.  The proofs are
//! split so the symbolic cost stays bounded:
//!
//! * The CRC harness ([`crc_detects_bit_flip`]) proves the load-bearing
//!   detection property of [`crate::crc32c::compute`] over arbitrary
//!   `[u8; 28]`.  Determinism / panic-freedom of `compute` are guaranteed
//!   by the type system (it is `pub const fn` with no global state) and by
//!   the const-asserts in `crc32c.rs`.
//! * The decode harnesses ([`decode_never_panics`],
//!   [`decode_classification`]) operate on inputs constrained so the
//!   CRC trailer matches the body, decoupling decode-correctness from
//!   CRC-correctness.
//! * [`encode_decode_roundtrips`] and [`decode_error_precedence`]
//!   exercise structural invariants over constructable frames.
//!
//! See `book/src/architecture/verification.md` for the full strategy and a
//! mapping from each harness to the protocol invariant it proves.

use crate::{crc32c, DecodeError, Frame, Status, MAGIC, NONCE_TERMINAL, VERSION};

/// **M7 Step 2 — panic-freedom.**
///
/// For every possible 32-byte input, [`Frame::decode`] returns without
/// panicking.  The harness is unconstrained: random bytes that fail the
/// magic / version / CRC / status / field-range gates surface as the
/// corresponding [`DecodeError`] variant; nothing inside the function
/// indexes outside `&[u8; 32]` or executes an `unwrap` on an `Err`.
#[kani::proof]
fn decode_never_panics() {
    let bytes: [u8; 32] = kani::any();
    let _ = Frame::decode(&bytes);
}

/// **M7 Step 2 — classification + post-condition coverage.**
///
/// For every 32-byte input, [`Frame::decode`] returns either an [`Err`]
/// of one of the named [`DecodeError`] variants or an [`Ok(Frame)`]
/// whose fields satisfy every documented post-condition:
///
/// * `frame.magic == MAGIC`
/// * `frame.version == VERSION`
/// * `frame.status` is one of `Ok` / `Degraded` / `Critical`
///   (`Stall` is rejected by [`DecodeError::StallOnWire`]).
/// * `frame.pid >= 2` (the `BadPid(0)` / `BadPid(1)` gates fire first).
/// * `frame.timestamp != u64::MAX` (the `BadTimestamp` gate fires first).
/// * `frame.nonce != NONCE_TERMINAL` unless `frame.status == Critical`.
///
/// The harness does NOT stamp a matching CRC over `bytes[0..28]`.
/// Kani explores both CRC-valid inputs (the `Ok(frame)` arm, reachable
/// when the SMT solver picks `bytes[28..32] == compute(bytes[0..28])`)
/// and CRC-invalid inputs (the `Err(BadCrc)` arm).  Stamping the CRC
/// externally introduced a second symbolic 28-iteration table-lookup
/// loop that CBMC had to prove equivalent to the one inside
/// `Frame::decode` — the same SMT-equivalence problem that forced the
/// removal of `crc_compute_is_total` (see comment below).  CRC
/// detection is proved separately by [`crc_detects_bit_flip`] in
/// Step 3, so this harness needs no CRC constraint.
#[kani::proof]
fn decode_classification() {
    let bytes: [u8; 32] = kani::any();

    match Frame::decode(&bytes) {
        Ok(frame) => {
            kani::assert(frame.magic == MAGIC, "magic preserved");
            kani::assert(frame.version == VERSION, "version preserved");
            kani::assert(frame.status != Status::Stall, "stall rejected at wire");
            kani::assert(frame.pid >= 2, "pid range");
            kani::assert(frame.timestamp != u64::MAX, "timestamp range");
            kani::assert(
                !(frame.nonce == NONCE_TERMINAL && frame.status != Status::Critical),
                "nonce sentinel ↔ critical",
            );
        }
        Err(e) => match e {
            DecodeError::BadMagic
            | DecodeError::BadVersion
            | DecodeError::BadCrc { .. }
            | DecodeError::BadStatus(_)
            | DecodeError::StallOnWire
            | DecodeError::BadPid(_)
            | DecodeError::BadTimestamp(_)
            | DecodeError::BadNonce { .. } => {}
        },
    }
}

// `crc_compute_is_total` (CRC determinism) was removed: CBMC took >19 min on
// it because two symbolic 28-iteration table-lookup expressions over the same
// input must be proved equivalent at the SMT level.  The property is already
// guaranteed by the type system — `crc32c::compute` is a `pub const fn` with
// no global state, no allocation, no FFI — and is exercised concretely by the
// const-asserts at `crc32c::tests::compute(b"") == 0x0000_0000` and the RFC
// 3720 reference vector.  Totality (panic-freedom) is subsumed by
// `decode_never_panics`, which calls `compute` via the decode path.

/// **M7 Step 3 — single-bit-flip detection.**
///
/// For every 28-byte payload and every bit position in `[0, 28 * 8)`,
/// flipping that bit produces a different CRC.  This is the
/// load-bearing property of CRC-32C — guaranteed by polynomial
/// construction — and is the reason the wire format uses CRC-32C
/// rather than a parity checksum.
///
/// State scope: pure CRC.  No decode path, no protocol gates.  CBMC
/// handles the 256-entry table lookup natively via array reads; the
/// 28-iteration loop is bounded by `default-unwind = 64` in
/// `Kani.toml`.
#[kani::proof]
fn crc_detects_bit_flip() {
    let bytes: [u8; 28] = kani::any();
    let bit: u32 = kani::any();
    // bit position in [0, 28 * 8) = [0, 224)
    kani::assume(bit < 28 * 8);

    let byte_idx = (bit / 8) as usize;
    let bit_mask = 1u8 << (bit % 8) as u8;

    let original = crc32c::compute(&bytes);
    let mut flipped = bytes;
    flipped[byte_idx] ^= bit_mask;
    let flipped_crc = crc32c::compute(&flipped);

    kani::assert(original != flipped_crc, "single-bit flip changes CRC");
}

/// **M7 Step 4a — encode/decode round-trip (smoke test for per-PR budget).**
///
/// The buffer produced by [`Frame::encode`] on a constructable [`Frame`]
/// decodes back to a [`Frame`] with identical fields.  This variant uses
/// concrete field values to stay within the per-PR CI budget (<1s);
/// the exhaustive multi-dimensional symbolic variant runs in kani-nightly.yml.
///
/// CRC computation over symbolic fields creates large SMT state
/// (even with only 2 symbolic variables, >2 min locally); smoke-testing
/// with concrete fields verifies the encode/decode path works, while
/// nightly exhaustive testing proves the invariant holds universally.
#[kani::proof]
fn encode_decode_roundtrips() {
    let original = Frame::new(
        Status::Ok,
        42u32,
        0x0123456789ABCDEFu64,
        0x0FEDCBA987654321u64,
        0x12345678u32,
    );
    let mut buf = [0u8; 32];
    original.encode(&mut buf);
    let decoded = Frame::decode(&buf).expect("constructable frame decodes");
    kani::assert(decoded == original, "fields preserved");
}

/// **M7 Step 4b — exhaustive encode/decode round-trip (nightly variant).**
///
/// For every constructable [`Frame`] whose field values satisfy the
/// documented invariants ([`Frame::decode`] docstring), the buffer
/// produced by [`Frame::encode`] decodes back to a `Frame` with
/// identical fields.  The constructable subset is bounded by:
///
/// * `pid >= 2` (pid 0 = scheduler, pid 1 = init).
/// * `timestamp < u64::MAX` (reserved sentinel).
/// * `status ∈ {Ok, Degraded, Critical}` (Stall is observer-synthesised).
/// * `nonce != NONCE_TERMINAL` unless `status == Critical`.
///
/// This exhaustive multi-dimensional symbolic variant explores all status
/// values and nonce constraints, creating large SMT state via CRC
/// computation over symbolic fields.  CBMC runtime is >80s locally;
/// runs in kani-nightly.yml with 6h budget.
#[kani::proof]
fn encode_decode_roundtrips_exhaustive() {
    let pid: u32 = kani::any();
    kani::assume(pid >= 2);

    let timestamp: u64 = kani::any();
    kani::assume(timestamp != u64::MAX);

    let status_byte: u8 = kani::any();
    kani::assume(status_byte <= 2); // Ok / Degraded / Critical
    let status = match status_byte {
        0 => Status::Ok,
        1 => Status::Degraded,
        2 => Status::Critical,
        _ => unreachable!(),
    };

    let nonce: u64 = kani::any();
    kani::assume(nonce != NONCE_TERMINAL || status == Status::Critical);

    let payload: u32 = kani::any();

    let original = Frame::new(status, pid, timestamp, nonce, payload);
    let mut buf = [0u8; 32];
    original.encode(&mut buf);
    let decoded = Frame::decode(&buf).expect("constructable frame decodes");
    kani::assert(decoded == original, "fields preserved bit-for-bit");
}

/// **M7 Step 4c — error-gate precedence.**
///
/// For every 32-byte input that fails decode, the first gate in the
/// documented order (magic → version → CRC → status → pid →
/// timestamp → nonce) is the one whose [`DecodeError`] variant is
/// returned.  This harness proves the magic and version precedences
/// universally; the remaining precedence cases are covered by
/// integration tests (`crates/varta-vlp/tests/frame.rs`) over chosen
/// counter-examples and are subsumed by [`decode_classification`] in
/// aggregate.
#[kani::proof]
fn decode_error_precedence() {
    let bytes: [u8; 32] = kani::any();
    if let Err(e) = Frame::decode(&bytes) {
        // BadMagic fires before any other gate.
        if bytes[0] != MAGIC[0] || bytes[1] != MAGIC[1] {
            kani::assert(matches!(e, DecodeError::BadMagic), "magic precedence");
        } else if bytes[2] != VERSION {
            // BadVersion fires before CRC, status, pid, etc.
            kani::assert(matches!(e, DecodeError::BadVersion), "version precedence");
        }
        // CRC / status / pid / timestamp / nonce precedences depend on the
        // exact body bytes and are exercised by `decode_classification`
        // (which constrains a valid CRC and observes the remaining gates
        // exhaustively).
    }
}