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

Makefile

@@ -560,14 +560,63 @@ fuzz-trophies:
 verify: verify-kani verify-creusot verify-smt verify-model verify-properties
 	@echo "✅ All formal verification passed!"
 
+# GH-212: this target used to report success while proving NOTHING. The crate
+# had not compiled under cfg(kani) for months — 19 errors in its own harness
+# files — and every invocation was suffixed `|| true`, so the failure was
+# swallowed. Contracts declaring `kani_harnesses:` were undischarged the entire
+# time while the gate read green. `pv validate` passing meant the contract was
+# well-formed, not that its obligations held.
+#
+# Two outcomes are now distinguished, because they do not mean the same thing:
+#
+#   BUILD failure  -> HARD FAIL. This IS the GH-212 defect: a harness that does
+#                     not compile can never prove anything. Caught by
+#                     --only-codegen in ~106s, without invoking the solver.
+#   No convergence -> UNPROVEN. Reported loudly, non-fatal. Bounded model
+#                     checking is exponential; "did not finish in the budget" is
+#                     not "the property is false", and failing the build on it
+#                     would make `make verify` permanently red — which is how a
+#                     gate teaches people to bypass it.
+#
+# MEASURED 2026-08-11, kani 0.67.0, 32-core box: none of these harnesses
+# converge. CBMC spends its time inside alloc::raw_vec / Layout / LayoutError —
+# Rust's ALLOCATOR — because every harness calls an escaping function that
+# returns a heap String. Shrinking the input bound does not help: 8, 4 and 2
+# characters all time out, so string LENGTH was never the bottleneck. Proving
+# these properties needs the escapers refactored onto caller-provided &mut [u8]
+# buffers so no allocation is reachable from a harness. Tracked separately.
+KANI_TIMEOUT   ?= 300
+KANI_HARNESSES := verify_escape_safety verify_variable_expansion_safety verify_injection_safety
+
 verify-kani:
 	@echo "🔍 Running Kani model checker..."
-	@if cargo +nightly kani --version >/dev/null 2>&1; then \
-		cargo +nightly kani --harnesses verify_parser_soundness --unwind 10 || true; \
-		cargo +nightly kani --harnesses verify_escape_safety --unwind 10 || true; \
-		cargo +nightly kani --harnesses verify_injection_safety --unwind 10 || true; \
-	else \
+	@if ! cargo +nightly kani --version >/dev/null 2>&1; then \
 		echo "⚠️  Kani not installed, skipping bounded model checking"; \
+		exit 0; \
+	fi; \
+	echo "  [1/2] cfg(kani) build — GH-212 regression guard"; \
+	if ! cargo +nightly kani -p bashrs --only-codegen; then \
+		echo "❌ bashrs does not compile under cfg(kani): every harness is unrunnable,"; \
+		echo "   and every contract declaring kani_harnesses: is undischarged."; \
+		exit 1; \
+	fi; \
+	echo "  [2/2] solving — budget $(KANI_TIMEOUT)s per harness"; \
+	unproven=0; \
+	for h in $(KANI_HARNESSES); do \
+		timeout $(KANI_TIMEOUT) cargo +nightly kani -p bashrs --harness $$h >/dev/null 2>&1; \
+		rc=$$?; \
+		if [ $$rc -eq 0 ]; then \
+			echo "    ✅ $$h VERIFIED"; \
+		elif [ $$rc -eq 124 ]; then \
+			echo "    ⏱  $$h UNPROVEN — no convergence in $(KANI_TIMEOUT)s"; \
+			unproven=$$((unproven+1)); \
+		else \
+			echo "    ❌ $$h FAILED (exit $$rc) — a property was refuted"; \
+			exit 1; \
+		fi; \
+	done; \
+	if [ $$unproven -gt 0 ]; then \
+		echo "  ⚠️  kani: $$unproven/$(words $(KANI_HARNESSES)) unproven (allocator-bound; see the comment above this target)"; \
 	fi
 
 verify-creusot:

rash/src/formal/kani_harnesses.rs

@@ -7,14 +7,17 @@
 mod kani_proofs {
     use crate::formal::semantics::{posix_semantics, rash_semantics};
     use crate::formal::{AbstractState, FormalEmitter, TinyAst};
+    // GH-212: `let s: String = kani::any()` is an E0277 — String is not (and
+    // cannot be) kani::Arbitrary. These harnesses had never been compiled.
+    use crate::kani_bounded::{any_bounded_identifier, any_bounded_string};
 
     /// Verify that echo commands preserve their output exactly
     #[kani::proof]
+    #[kani::unwind(7)]
     fn verify_echo_semantic_equivalence() {
-        // Create a bounded string for the argument
-        let arg: String = kani::any();
-        kani::assume(arg.len() <= 10); // Bound the string length
-        kani::assume(arg.chars().all(|c| c.is_ascii_alphanumeric())); // Simple chars only
+        // Bounded at 6, not the original's 10: the state space is 62^N, and the
+        // bound must be justified by a measured runtime rather than a wish.
+        let arg = any_bounded_string::<6>();
 
         let ast = TinyAst::ExecuteCommand {
             command_name: "echo".to_string(),
@@ -48,21 +51,13 @@ mod kani_proofs {
 
     /// Verify that environment variable assignments are preserved
     #[kani::proof]
+    #[kani::unwind(6)]
     fn verify_assignment_semantic_equivalence() {
-        // Create bounded strings for name and value
-        let name: String = kani::any();
-        let value: String = kani::any();
-
-        // Bound the strings
-        kani::assume(name.len() > 0 && name.len() <= 8);
-        kani::assume(value.len() <= 10);
-
-        // Ensure valid variable name
-        kani::assume(name.chars().all(|c| c.is_ascii_alphabetic() || c == '_'));
-        kani::assume(
-            name.chars().next().unwrap().is_ascii_alphabetic()
-                || name.chars().next().unwrap() == '_',
-        );
+        // any_bounded_identifier encodes the leading-char rule the original
+        // spelled out with two assumes (and an `.unwrap()` on `next()` that
+        // would have been reachable had len == 0 slipped through).
+        let name = any_bounded_identifier::<4>();
+        let value = any_bounded_string::<5>();
 
         let ast = TinyAst::SetEnvironmentVariable {
             name: name.clone(),

rash/src/kani_bounded.rs

@@ -0,0 +1,54 @@
+#![cfg(kani)]
+//! Bounded symbolic values for Kani harnesses.
+//!
+//! Kani cannot generate a `String` or `&str`: neither implements
+//! `kani::Arbitrary`, and neither can — they are unbounded heap types, and
+//! bounded model checking needs a finite state space. Every `let s: String =
+//! kani::any();` in this repo was therefore an `E0277`, which is most of the 19
+//! errors that made the crate uncompilable under `cfg(kani)` (GH-212). Those
+//! harnesses had never been compiled, so nobody found out.
+//!
+//! The standard model is a fixed-size byte array (which IS `Arbitrary`) plus a
+//! symbolic length and an alphabet constraint. `N` is the real cost knob: the
+//! solver explores `|alphabet|^N` strings, so keep it small and raise it only
+//! with a measured runtime.
+
+/// A symbolic `String` of length `0..=N` over ASCII alphanumerics.
+///
+/// Pair with `#[kani::unwind(N + 1)]` on the harness — the loop below is what
+/// needs the unwind bound, and an unwind that is too low is reported by Kani as
+/// an unwinding-assertion failure rather than silently under-approximating.
+pub fn any_bounded_string<const N: usize>() -> String {
+    let bytes: [u8; N] = kani::any();
+    let len: usize = kani::any();
+    kani::assume(len <= N);
+
+    let mut s = String::with_capacity(len);
+    for &b in bytes.iter().take(len) {
+        kani::assume(b.is_ascii_alphanumeric());
+        s.push(b as char);
+    }
+    s
+}
+
+/// A symbolic POSIX-ish identifier of length `1..=N`: `[A-Za-z_][A-Za-z0-9_]*`.
+///
+/// Separate from `any_bounded_string` because the leading character carries a
+/// different constraint, and folding that into one function would either
+/// over-constrain ordinary strings or under-constrain identifiers.
+pub fn any_bounded_identifier<const N: usize>() -> String {
+    let bytes: [u8; N] = kani::any();
+    let len: usize = kani::any();
+    kani::assume(len >= 1 && len <= N);
+
+    let mut s = String::with_capacity(len);
+    for (i, &b) in bytes.iter().take(len).enumerate() {
+        if i == 0 {
+            kani::assume(b.is_ascii_alphabetic() || b == b'_');
+        } else {
+            kani::assume(b.is_ascii_alphanumeric() || b == b'_');
+        }
+        s.push(b as char);
+    }
+    s
+}

rash/src/lib.rs

@@ -113,6 +113,9 @@ pub mod gates;
 pub mod installer;
 /// Intermediate representation for transpilation
 pub mod ir;
+/// Bounded symbolic values for Kani harnesses (see GH-212)
+#[cfg(kani)]
+pub mod kani_bounded;
 /// Shell script linting with ShellCheck-equivalent rules
 pub mod linter;
 /// Makefile parsing and purification