Mixed-width i32/i64 Select forces verification reverts: coverage loss is counted but not attributed, and the free verify entry point is panic-unsafe

[avrabe]

Two narrow, related gaps found while measuring Tier-2 slice-1 coverage (#330). Neither is a crash in the optimizer, and this is explicitly not a recurrence of #98/#145 — I want that stated up front, because that is what I assumed before checking.

What is actually happening

On tests/fixtures/issue254-records-fused.wasm, 4 of 724 functions (#132, #142, #161, #182) panic inside the solver bindings during SMT encoding, before any solver is consulted:

fn#132  z3/src/ast/mod.rs:601   SortDiffers { left: (_ BitVec 32), right: (_ BitVec 64) }
fn#142  z3/src/ast/bool.rs:70   called `Option::unwrap()` on a `None` value
fn#161  z3/src/ast/bool.rs:70   called `Option::unwrap()` on a `None` value
fn#182  z3/src/ast/mod.rs:601   SortDiffers { left: (_ BitVec 32), right: (_ BitVec 64) }

mod.rs:601 is a mixed-width BV binop; bool.rs:70 is the .unwrap() inside Bool::ite, which returns NULL when the arms have different sorts. All four functions contain Select together with mixed i32/i64 — Select lowers to Bool::ite, so the two signatures are one root cause reached by two constructors. Reproduced from a cold checkout of main @ 3375f91; independent of #330.

The optimizer does not crash on this, and that is by design. TranslationValidator::verify wraps encode/check in catch_unwind (two sites, verify.rs ~3028/~3047) and converts a solver-internal panic into a clean revert. The behaviour is already documented at verify.rs:1375-1391, which names this exact case — "a SortDiffers BitVec-64-vs-32 width mismatch, or an unwrap()-on-None deep in the bindings … the revert is correct/conservative" — and install_z3_panic_filter exists to suppress the resulting stderr noise. Verified all of that against the source rather than taking it on report.

So the conservative behaviour is correct. The two gaps are elsewhere.

Gap 1 — coverage loss is counted but not attributed

Those 4 functions silently lose verification and are reverted. The only trace is an aggregate record_revert count: nothing records which functions were never verified, or why.

That is a real tension with the charter's "no silent failures". A user reading a successful loom optimize has no way to learn that four functions in their module were not verified at all — and on an i64-heavy module the same mechanism can revert far more. The optimizer is behaving conservatively, but it is not being honest about its own coverage, which is the same species of problem as a claim not backed by a check.

Suggested shape: attribute reverts per-function with a reason, and surface the count (and ideally the list) in the verification summary rather than only in an internal counter. This composes with the --emit-* reporting surfaces rather than needing new machinery.

Gap 2 — the public free function is panic-unsafe, and the asymmetry is undocumented

pub fn verify_function_equivalence has no catch_unwind. Any direct caller inherits the panic, while a caller going through TranslationValidator::verify gets a clean revert. Both are public API surface, the difference is invisible from the signature, and nothing says so.

Suggested: either give the free function the same catch_unwind treatment, or document the asymmetry explicitly at the definition, so a future caller (or a future migration slice) does not discover it by crashing.

Reproduction

No committed test triggers it. Add a probe to loom-core/src/verify.rs:

#[cfg(all(test, feature = "verification"))]
mod repro {
    use super::*;
    use std::panic::{AssertUnwindSafe, catch_unwind};
    #[test]
    fn repro() {
        let bytes = std::fs::read("tests/fixtures/issue254-records-fused.wasm").unwrap();
        let m = crate::parse::parse_wasm(&bytes).unwrap();
        for i in [132usize, 142, 161, 182] {
            let f = &m.functions[i];
            let r = catch_unwind(AssertUnwindSafe(|| verify_function_equivalence(f, f, "repro")));
            println!("fn#{i}: panicked={:?}", r.is_err());
        }
    }
}

Run with --features verification --lib repro -- --nocapture --test-threads=1. Backend mode is irrelevant — this is before solver selection.

Note sem.loom.wasm does not panic (4 functions, 0 panics); an earlier report of mine naming it was wrong.

Refs #330, #313