fix(verify): #347 bound array-modelled memory operations, and refuse what cannot be verified

[avrabe]

Stacked on #349 → #344. Bases retarget as each merges.

Closes the shipping blocker in #347. 463 KB fused module: >455 s (killed) → 45 s, exit 0, output valid.

Root cause — measured, and not what I expected

Bisected to one pass (every other pass ≤1s), then confirmed it was the verification not the transform (LOOM_Z3_MAX_INSTRUCTIONS=1 → 1s). Then profiled:

14172  loom_core::optimize::inline_functions
13725   TranslationValidator::verify -> Z3_solver_check      97%
 5290    smt::theory_array_base::propagate                   40%
 3849     assert_store_axiom2_core

The solver's array theory — the memory model — instantiating store axioms pairwise, so cost is quadratic in memory accesses per body. Only the inliner triggers it, for a structural reason: it's the one pass that concatenates callee bodies into a caller, so the one pass that multiplies memory accesses per function. That's why size, functions, blocks, loops and br_table all failed to discriminate — the 39s control exceeds the hanging module on every one.

I went in with a different hypothesis — the acyclic-CF executor from #219, which runs only for inline_functions and fit the evidence perfectly. The profile disproved it. A fix for that would have shipped and changed nothing.

Two decisions, both reached by measurement

Exceeding the bound REVERTS, unlike the instruction bound. Returning Ok would accept a transform nothing verified — thousands per module at this bound. Refusing costs optimization and costs nothing in safety. The instruction bound still keeps; that inconsistency is left visible rather than quietly harmonised.

Tiny bodies are exempt, and that is not a nicety. The naive bound broke #219:

	required bound
#219 seam dissolution	≥ 4
#347 module completes	≤ 2

Irreconcilable. The first implementation silently regressed shipped, silicon-validated seam work — caught only because those tests exist. Exempting bodies under an instruction floor resolves it, since the seam inlines are tiny and the pathological ones are inlined-large. Result: 45s, seams intact, and slightly better coverage than without the exemption (49.8% vs 45.2%).

What this is not

Not a solution. It buys termination by declining the hardest obligations. They're discharged only when the memory model stops being the incumbent's array theory — #313 slice 5.

Not a timeout, and not for want of trying. The solver's timeout is wired (LOOM_Z3_TIMEOUT_MS, default 5000) and measurably does not bound this: at 100 ms the pass still exceeded 120 s, because the time goes into axiom instantiation, not the search a timeout guards. A wall-clock budget is also ruled out on principle — it would make which functions got verified depend on machine speed, so the same input could produce different output (REQ-14).

Measured cost on a normal module

0.47% larger output; 21% of the optimization gain foregone. Stated rather than buried — this is a real regression traded for 97/100 components becoming usable at all.

Tests

Counter correctness (including through block/if bodies, so stores can't hide under the bound), the float/partial-width exclusion, plus the exemption and its control — a large memory-dense body must not be exempt, without which the bound could never fire.

loom-core --lib 539/539 (default and both) · 410/410 --no-default-features · --test verification 47/47 · loom-cli 21/21.

Verifies TEST-347-MEMORY-OP-BOUND