minerva 0.2.0

//! Kani proof harnesses for the *heap-free* fragment of the `VersionVector` wire
//! boundary (S86, revised under the owner's Kani-scope ruling in R-9).
//!
//! Compiled only under `cargo kani` (`cfg(kani)`). Kani is deliberately kept off
//! every path that constructs the `BTreeMap`: symbolic heap structure (insert,
//! node arrays, iteration, drop glue) is what a bit-blasting solver cannot afford,
//! and no determinism patch changes that (the map is already deterministic; the
//! cost is modeling, not ordering). The map-touching parser laws are covered by
//! the shaped property tests in `tests/wire/vector/properties.rs` and driven
//! unbounded by the fuzz targets; the deductive rung for heap-backed code is
//! chartered for Creusot (ruling R-9). What remains here is exactly the fragment
//! the solver is good at: pure arithmetic and the pre-map rejection path.

use super::VersionVector;

/// The PRD 0007 IMPORTANT-box arithmetic, discharged totally: the required
/// frame-length computation `5 + count * 12` cannot overflow `u64` for any
/// claimed `u32` count, so the O(1) bound check is sound on every target width.
#[kani::proof]
fn length_check_arithmetic_cannot_overflow() {
    let count: u32 = kani::any();
    let entries = u64::from(count)
        .checked_mul(12)
        .expect("u32 count times entry width fits u64");
    let frame_len = 5u64
        .checked_add(entries)
        .expect("header plus entries fits u64");
    let _ = frame_len;
}

/// Every input shorter than the five-byte header is rejected without panicking,
/// for all lengths zero through four and all contents. This path returns before
/// the map is ever constructed, so it stays within Kani's heap-free scope.
#[kani::proof]
#[kani::unwind(6)]
fn from_prefix_rejects_sub_header_input() {
    let bytes: [u8; 4] = kani::any();
    let len: usize = kani::any();
    kani::assume(len <= bytes.len());
    assert!(VersionVector::from_prefix(&bytes[..len]).is_err());
}