feat(stats): #331 report what verification established, not only what it caught

[avrabe]

Stacked on #343 (both touch main.rs and verify.rs). Base will retarget to main once #343 merges.

Closes #331's Gap 1. Requested directly: "maybe we need to provide some stats during the operation."

The gap

--stats printed revert counts and nothing else. Those answer "how often did verification catch something?" — they cannot answer "how much was verified at all?", because they have no denominator. And the outcome that matters most is invisible to them by construction: a transform kept without a proof does not revert, so it never appears in a revert count.

loom keeps such transforms deliberately and for stated reasons. That's defensible. Reporting success without saying it happened is not — REQ-3 is not satisfied by a failure that is merely not an error.

The mislabel

Worse than the missing denominator. The solver size-threshold bypass recorded itself with record_revert("<pass>/z3-size-skipped") and then returned Ok(()) — which the caller reads as acceptance. So --stats printed "N function(s) reverted" for functions that shipped unverified. On the in-tree 724-function fixture, that was 18 attempts.

A stat that names the wrong outcome is worse than no stat: it reads as evidence verification did its job, in precisely the case where it did not run.

The machinery already existed

VerificationCoverage has carried the full taxonomy — verified / skipped_loops / skipped_memory / skipped_unknown / failed / error — with skip_reason() returning ready-made strings. compute_verification_coverage is pub, implemented, and its doc comment shows the exact summary line it was meant to produce. It has zero non-test callers. A comment in the lenient path even points at it: "the structured VerificationCoverage tracker records counts." Nothing read them.

This PR does not call it — that would re-verify every function and double the work. Counts accumulate during the run that actually happens.

After

🔍 Verification Coverage
─────────────────────────────────────────
  Proven:  7283/7575 attempts (96.1%)
  Kept WITHOUT proof: 18 attempt(s)
    body over the solver size threshold  18
  Rejected (reverted): 274
  (one attempt = one function, one pass — not one function)

  ⚠️  Not every transform in this output carries a proof.

The denominator is labelled honestly: with 15 passes and --islands N the same function is verified many times, so it counts attempts, and says so rather than implying a function count.

Classification uses unverifiable_reason, extracted from the predicate the verifier already applied inline — so the accounting cannot drift out of agreement with the decision it describes.

proven_percentage() returns None for zero attempts rather than 100.0. 0/0 divides out to "no failures", which is exactly the vacuous claim this reporting exists to prevent.

The disabled-feature stub, fixed first

compute_verification_coverage's #[cfg(not(feature = "verification"))] arm reported every function as verified for a build that verified nothing — "they're assumed correct". That is #332's defect one layer deeper: pre-loaded rather than fired, and it would have fired on whoever wired the honest path. Which is this PR.

Tests

Reachability is the asserted property (#289): the kept-without-proof bucket must be reached on the fixture and attributed by name, or every other assertion would pass for an implementation that never records it. Paired with a positive control asserting a fully-proven run does not carry the warning — a caveat shown unconditionally carries no information.

loom-core --lib 534/534 (also under LOOM_VERIFY_BACKEND=both, no divergence) · --test verification 47/47 · loom-cli 18/18 · fmt + clippy clean.

Verifies TEST-331-VERIFICATION-COVERAGE-IS-REPORTED

[avrabe]

Review pass found two defects in this PR — both the shape it exists to fix

1. The void auto-pass was counted as proven

The wrapper classified attempts by re-deriving unverifiable_reason over the instruction list. That predicate cannot see acceptances decided by the encoding result rather than the function's shape — and there is one: (Ok(None), Ok(None)), the void-function auto-pass, whose own comment says the equivalence is "vacuous" and that memory/global writes are not modelled at all.

So a vacuous pass was counted as a proof — inflating the coverage number with exactly the empty checks that number exists to expose.

Classification now happens at the decision site, via a thread-local note the wrapper reads back. An accounting layer that re-derives its subject can silently disagree with it.

Measured after the fix: the arm fired 0 times — not on a module of nothing but void functions (including an empty one and one writing a global), and not on the 724-function fixture. The encoder returns Ok(Some(..)) for void bodies, so the arm appears unreachable in practice. The 7283/7575 (96.1%) headline is unchanged and stands. The classification is kept as defensive and documented as unexercised rather than claimed as covered.

Audited every other Ok(true) in the same function: k-induction success, the seam's Proven, and SatResult::Unsat are genuine discharges; SatResult::Unknown and both encode failures already return Err. The k-induction-disabled branch is dead (the const is true) but now notes itself, since it would be an assumption if ever enabled.

2. An acceptance criterion nothing ran

The rivet artifact asserted "a build without the verification feature does not report functions as verified" and was marked verified — while both of its steps compiled the feature in. That arm had never been built. A claim asserted by no runnable check, inside the change whose entire subject is that defect class.

Fixed three ways:

• the disabled arm records into a new not_attempted bucket rather than borrowing verification_error. Reporting a timeout that never happened is no better than reporting a proof that never happened; every other bucket asserts something specific, so "nothing ran" needed its own.
• tests compiled only when the feature is off, plus a matching rivet step.
• confirmed discriminating: with the old record_verified() restored, the test fails on the verified-count assertion.

Verification

loom-core --lib 534/534 (default and LOOM_VERIFY_BACKEND=both) · 410/410 --no-default-features · --test verification 47/47 · loom-cli 17/17 · fmt + clippy clean.