fix: #346 output validation + data count section, and #347 memory-op bound

[avrabe]

Scope note: this PR now carries two fixes. #350 (the #347 memory-op bound) auto-merged into this branch, so #346 and #347 land together. Both are v1.4.1 scope, both have their own rivet artifact, and CI is green on the combined head. #350's own description carries the full #347 write-up.

Closes #346 · closes the shipping blocker in #347 · closes the CLI half of #345.

---

Part 1 — #346: never write a module loom has not validated

Reproduces from 79 bytes

(module (memory 1) (data $d "hello")
  (func (export "init") (param i32)
    local.get 0  i32.const 0  i32.const 5
    memory.init $d
    data.drop $d))

$ loom optimize dc.wasm -o out.wasm
✅ Optimization complete!     $ echo $? -> 0
$ wasm-tools validate out.wasm
error: data count section required (at offset 0x2d)

The section was never emitted at all

Not "dropped": there was no reference to the data count section anywhere in loom-core. The parser read MemoryInit/DataDrop; nothing ever wrote the section they require. Now emitted (id 12) between element and code whenever those instructions survive.

The guarantee was unreachable

The #257 MANDATORY AUTHORITATIVE OUTPUT-VALIDATION BACKSTOP, whose comment states it is "the systemic guarantee that loom can NEVER emit structurally invalid wasm", lives inside optimize_module. The CLI does not call it — it drives the passes directly (#345). Grepping loom-cli/src/main.rs for validate: three hits, all comments.

All three write paths — serial, islands, component — now pass through one gate. On failure the original is written instead, but only after the original is itself proven valid, and the exit code is non-zero.

Confirmed discriminating twice, by reverting each half: without the encoder fix the memory.init test fails on "data count section required"; without the gate the CLI writes the invalid module and exits 0.

---

Part 2 — #347: bound the quantity that actually drives solver cost

463 KB fused module: >455 s (killed) → 45 s, exit 0, output valid.

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

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

The solver's array theory instantiating store axioms pairwise — quadratic in memory accesses per body, which inlining multiplies by concatenating callees. LOOM_Z3_MAX_INSTRUCTIONS bounds the wrong quantity.

I went in with a different hypothesis (the #219 acyclic executor, which runs only for inline_functions and fit the evidence). The profile disproved it.

The bound REVERTS rather than keeps — unlike the instruction bound, whose keep-behaviour is left untouched and the inconsistency stated rather than quietly harmonised.

Tiny bodies are exempt, and that is not a nicety. The naive bound silently broke #219's silicon-validated seam dissolution: seams need bound ≥4, #347 needs ≤2 — irreconcilable. The exemption resolves it, with better coverage (49.8% vs 45.2%).

What it is not: not a solution (the obligations are discharged only by #313 slice 5), and not a timeout — the solver's timeout is wired and at 100 ms the pass still exceeded 120 s. A wall-clock budget is ruled out by REQ-14.

Measured cost on a normal module: 0.47% larger output, 21% of the optimization gain foregone.

---

Verification

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

Verifies TEST-346-OUTPUT-IS-VALIDATED-BEFORE-IT-IS-WRITTEN, TEST-347-MEMORY-OP-BOUND