Kani bounded model checker — dsfb-atlas v2.0.0
=============================================

Harness: `dedup_collision_iff_repeated_body`
   Source: src/dedup.rs (gated behind `#[cfg(kani)]`)
   Bound:  unwind = 5

Claim under verification:
   For any sequence of `Dedup::record(id_i, body_i)` calls (i in 0..n,
   n in 0..=3, body alphabet {alpha, beta, gamma}), the finalize report's
   `collisions` field is non-empty if and only if some pair (body_i,
   body_j) with i != j is byte-equal.

Invocation:
    cd crates/dsfb-atlas
    cargo install --locked kani-verifier && cargo kani setup
    cargo kani --harness dedup_collision_iff_repeated_body

Pass criterion: output ends with `VERIFICATION:- SUCCESSFUL`; no
`Failed Checks` lines; no unwind assertions firing within the bound.

This file is regenerated by `audit/scripts/kani.sh`.

Status (latest run): PASS — verification successful.
