fix(kani): make the crate compile under cfg(kani), and stop swallowing the failure (GH-212)

[noahgift]

Closes #212. Follow-up filed as #220.

cargo +nightly kani -p bashrs --harness <any> failed to build the crate — 19 errors in bashrs's own harness files. So no harness could run, including newly added correct ones, and every contract declaring kani_harnesses: was undischarged. pv validate passing meant the contract was well-formed, not that its obligations held.

It stayed invisible because every kani invocation in the Makefile was suffixed || true.

Three problems, only the first a typo

1. kani::assert! is not a macro Kani exports. Kani intercepts the standard assert!/assert_eq!.
2. escape_shell_value, is_valid_rust0, validate_rust0_ast do not exist in this crate, and there's no evidence they ever did.
3. String/&str are not kani::Arbitrary — and cannot be. They're unbounded heap types; BMC needs a finite state space. Every let s: String = kani::any(); was an E0277. Added crate::kani_bounded: fixed byte array + symbolic length + alphabet constraint.

Two harnesses deleted, not repaired

Compiling them would have produced proofs of nothing:

• verify_array_bounds_safety — asserted true on one branch; on the other, that a format! literal contains "-lt". No code under test was ever reached.
• verify_parser_soundness — called the real parser on a symbolic string, checked against the two functions that don't exist. Not tractable under BMC even if they were supplied.

Two more were near-vacuous and now call the real escapers: one asserted properties of a format! literal that hold even if the escaper is the identity function; the other checked a toy re-implementation local to the file against a toy oracle.

A harness that cannot fail is worse than a missing one — it consumes the verification budget and reports success.

verify-kani now separates two different things

outcome	behaviour	why
build failure	hard fail	This is the GH-212 defect. Caught by --only-codegen in ~106s, no solver needed.
no convergence	UNPROVEN, reported, non-fatal	"Didn't finish in budget" ≠ "property is false". Failing here would make make verify permanently red — which is how a gate teaches people to bypass it.

Verified differentially

fixed                → --only-codegen: 0 errors, 106s; target exits 0
E0277 reintroduced   → target exits 1: "does not compile under cfg(kani)"

What this does NOT claim

None of the three surviving harnesses converge. Measured and reported rather than papered over: CBMC spends its time in alloc::raw_vec / Layout / LayoutError — Rust's allocator — because every harness calls an escaper returning a heap String. Bounds of 8, 4 and 2 characters all time out, so string length was never the bottleneck.

Fixing that means giving the escapers an allocation-free core (escape_shell_string_into(&str, &mut [u8])) for harnesses to target. That changes the public signature of functions every emitted script depends on, so it's filed as #220 rather than riding along here.

What this PR buys is that the harnesses now build — the precondition for any of it, and the thing that was silently false for months.

🤖 Generated with Claude Code