fix(cli): #332 loom verify must not report success while it verifies nothing

[avrabe]

Closes #332. Also closes #331's Gap 2.

#332 — the vacuous gate

loom verify printed ✓ LOOM Verification, never opened its argument, and exited 0. All four negative controls from the report reproduce exactly on main:

input	before	after
add.wasm (wrong type entirely)	✓ exit 0	error: expected an ISLE rule file — exit 2
/nonexistent/nope.isle	✓ exit 0	error: no such file — exit 2
junk.isle (arbitrary text)	✓ exit 0	warning: nothing was verified — exit 2
empty file	✓ exit 0	warning: nothing was verified — exit 2

The ⚠️ not yet implemented line was present and honest, but it sat below the checkmark and never reached the exit code — the only thing automation reads.

There is now no exit-0 path

Input validation runs first and reports real errors, but passing it establishes only that the argument is a plausible ISLE file — never that anything was verified. The two outcomes stay textually distinct for that reason: a validation failure says error:, a validated file still says warning: nothing was verified. Everything goes to stderr; stdout stays empty, so a caller redirecting it gets nothing that could be mistaken for a result.

Exit code 2 is deliberately distinct from the 1 an ordinary failure produces, so "this build cannot verify anything" stays distinguishable from "verification ran and rejected something" once Phase 5 makes the second outcome possible. A test pins that they don't collide.

The load-bearing test

a_well_formed_isle_file_still_does_not_report_success. Every other assertion here would still hold for a validator that rejects bad input and then reports success for good input — the same vacuous gate wearing a coat.

Docs

The two references in docs/analysis/synth-architecture.md advertised the command in a two-wasm form the CLI has never accepted. Fixing the exit code while a doc still recommended it would leave half the defect in place; a test now fails if any doc line invokes loom verify as runnable.

#331 Gap 2 — same root, opposite direction

verify_function_equivalence propagated solver-internal panics while TranslationValidator::verify caught them and reverted cleanly — two public entry points behaving differently, with nothing in either signature saying which.

Now caught and reported as Err — never Ok(false): a counterexample is a positive finding of inequivalence, and a panic is not that.

Confirmed discriminating rather than assumed. With the fix reverted, the new test reports propagated 4 panic(s) — precisely functions #132, #142, #161, #182, independently reproducing #331's measurement. The test also asserts the panic path is still reachable (#289), so it cannot decay into a guard over nothing.

Semver note

exit 0 → exit 2 is a breaking CLI change on a subcommand. Blast radius is zero — it is wired nowhere in the org, and it is a pre-Phase-5 placeholder that never did anything. Called out here rather than left implicit.

Also answered: the 23× expansion

Gale's side-observation (41 B → 942 B) is not an optimizer defect. It is a fixed-size wsc.transformation.attestation custom section — 967 bytes measured via wasm-tools objdump. Negligible on real modules; 23× on a 41-byte one. No change needed.

Tests

7 new CLI integration tests (via CARGO_BIN_EXE_loom — no new dependency) + 1 new verification test.
cargo test -p loom-cli 7/7 · --test verification 47/47 · fmt + clippy clean.

Verifies TEST-332-VERIFY-REPORTS-NO-VACUOUS-SUCCESS, TEST-331-FREE-VERIFY-ENTRY-POINT-IS-PANIC-SAFE