v1.1.5 — Inline a local callee even when the caller calls an import (#153)

Bug-fix release. Closes the gale follow-up (#153): on v1.1.4,
inline_functions reverted the inline of a local callee whenever the
caller also called an imported function — blocking the gale C↔Rust
seam, where z_impl_k_sem_give inlines gale_k_sem_give_decide but also
calls 5 env:: kernel imports.

Root cause — a function-index-space confusion (not a verifier gap)

Call(func_idx) uses the full WebAssembly function index space:
imported functions occupy 0..num_imported_funcs, local functions
follow. But the inliner built function_sizes keyed by local index
while call_counts keyed by full index, and indexed the local-only
all_functions table with the full func_idx. With an import present
the spaces diverge — the import's index collides with a local function's
slot, so the inliner treated a void imported call as a call to local
function 0, emitted a local.set to bind its parameters with no
argument on the stack, and produced a malformed body. The translation
validator correctly rejected the bad encoding (Stack underflow in LocalSet), so the whole inline reverted.

The report hypothesised a missing verifier model for imported calls;
ground-truthing showed the real bug was upstream — the inliner emitting
nonsense — and the verifier was right to reject it.

Fix

• Compute num_imported_funcs once per pass iteration.
• Key function_sizes and the candidate gate by the full index
  (matching call_counts).
• Exclude imported indices from inline candidates — they have no body.
• Map full→local (func_idx - num_imported_funcs) when indexing the
  local-function table; an imported index yields None → the call is
  kept untouched. The offset is threaded through the block/loop/if
  recursion.
• Modules with no imported functions are unaffected (offset 0).

Validation

• New regression test test_inline_caller_with_imported_call: the import
  call is preserved while the local i64 callee is inlined and verified.
• 386 lib tests pass; the #151 i64/i32 repros still inline; the #153
  repro inlines (valid output); real gale wasm + the full default pipeline
  dogfood clean.
• Integration suite shows exactly the 7 pre-existing #150 LICM/DCE
  failures — nothing new.

Known limitations

• The 7 pre-existing LICM/DCE integration-test failures (#150) remain,
  unrelated to this change (they fail identically on v1.1.1).

Closes #153.

v1.1.4 — Verified i64 (and all-type) inlining (#151)

Bug-fix release. Closes the gale follow-up (#151): on v1.1.3,
loom optimize --passes inline reverted every i64 inline — even a
trivial i64.add callee — because the Z3 translation validator could
not prove i64 inline-equivalence. This made the verified inliner a no-op
for i64 modules and blocked the gale C↔Rust seam (z_impl_k_sem_give
inlining gale_k_sem_give_decide -> i64).

Root cause (deeper than the report)

Ground-truthing falsified the "i64-specific" framing — an i32 control
reverted too. The validator modeled call F as an opaque
uninterpreted function pure_call_F(args). That encoding proves two
identical calls equal (which CSE / directize rely on) but can never
prove a call equal to its own inlined body — so the original (with the
call) and the optimized (with F inlined) never matched, and every
inline was reverted as "unproven". i32 was a no-op for the same reason;
the report only saw i64 because that was the gale use case.

Fix

• By-body call modeling. When F is a pure, no-trap, leaf,
  straight-line, single-result callee, the validator now models
  call F(args) by symbolically executing F's own body on the
  argument bit-vectors — by F's definition — instead of an opaque
  symbol. Original and optimized then compute the identical expression
  and Z3 proves them equal, so the inline is kept with a real proof.
  Callees outside that whitelist fall back to the conservative opaque
  encoding (at worst a spurious revert, never an unsound accept).
• Consistency. Both the direct call F and the resolved
  call_indirect paths use the by-body model, keeping directize's
  call_indirect ⇔ call F equivalence intact.
• i64 in nested blocks. The nested-block SMT interpreter now models
  the full i64 arithmetic / bitwise / comparison / eqz set plus the
  total width conversions (i64.extend_i32_{s,u}, i32.wrap_i64),
  fixing a latent verification gap where every i64 op inside a
  block/loop/if was an opaque 32-bit symbolic.

Soundness

A new guard test proves both directions: a correct x+1 inline of
add1 is proven equivalent, and a deliberately wrong x+2 "inline" is
rejected (counterexample). The previously-#[ignore]'d i64-inline
test (#147 follow-up) is re-enabled and passing. 385 lib tests pass;
real gale wasm + the full default pipeline dogfood clean.

Known limitations

• The 7 pre-existing LICM/DCE integration-test failures (#150) remain —
  unrelated to this change (they fail identically on v1.1.1).
• Real verified inlining is enabled for the straight-line integer
  callee whitelist; widening it (rotates, popcount, memory/global
  readers, control flow) is gated follow-up work, each addition with its
  own soundness argument.

Closes #151.

LOOM v1.1.3 — fix #147 i64 inline livelock (gale-ffi)

Headline

Closes #147: on v1.1.2, loom optimize --passes inline hung indefinitely on i64-heavy modules (gale-ffi: z_impl_k_sem_give u64-unpack + caller) — 0 panics, no completion. This was the last loom-side gate for gale's verified cross-language-LTO route.

Root cause — a livelock, not slow Z3

The earlier "i64 Z3 verification is slow" diagnosis (v1.1.2) was wrong. Verify returns in microseconds. The real bug: inline_functions loops "until no inline candidate remains," but a candidate whose inline the verifier reverts (an i64 function whose inline-equivalence can't be proven) stays a candidate every iteration — its call site is restored on revert — so the pass live-locked: inline → revert → inline → … forever. It surfaced only because v1.1.2's #145 fix removed the SortDiffers panic that used to abort the pass.

Fixed

• inline_functions terminates when an iteration keeps no inline (no net progress), with a 64-iteration hard cap as a backstop. Legitimate inlining is unchanged.
• The loom optimize --passes inline gale repro now completes (exit 0; output passes wasm-tools validate; the unprovable i64 function is reverted once, then the pass terminates).
• Four of the five previously-#[ignore]'d i64 inline tests run again (in milliseconds). The fifth asserts the i64 helper is inlined, which the verifier soundly reverts as unprovable — real verified i64 inlining remains a follow-up.

Verify

loom optimize merged.wasm --passes inline --stats -o out.wasm   # completes; no hang

Notes

• This release also makes loom's CI Test matrix complete for the first time (it previously never finished — cancelled by the upstream Rocq job, then hung by this livelock). That exposed 7 pre-existing LICM/DCE integration-test failures (they fail identically on v1.1.1) — tracked in #150, unrelated to this fix.
• Rocq Formal Proofs remains red (pre-existing upstream rules_rocq_rust toolchain breakage). Substantive gates green: Z3 Verification Build, Differential Testing, Build ×3, Clippy, Format, WASM Build, Validate WebAssembly Output, Rivet.

LOOM v1.1.2 — fix #145 gale i64 SortDiffers crash

Headline

Bug-fix release closing #145: loom optimize panicked with SortDiffers { BitVec 64 vs 32 } (plus unwrap()-on-None through other z3 binding sites) on i64-heavy modules (gale-ffi / compiler_builtins), reverting essentially every function (inliner no-op) and emitting 21 MB+ of stderr.

Fixed

• No more crash. The Z3 translation validator's two symbolic executors hardcoded BitVec32 for uninitialized locals/stack/globals and applied unmatched binops, so a real i64 value meeting a 32-bit-modeled slot tripped a width mismatch deep in z3. The dormant match_bv_widths helper (added but never wired in by the #98/#99 fix) is now applied at every binop + comparison operand site in both executors. Sound: a valid wasm binop's operands are equal-width by construction, so matching only repairs a model artifact. The equivalence checks are not width-matched (that could approve a non-equivalent transform) — they bail to a conservative revert on any mismatch.
• No more 21 MB stderr flood. A Once-installed, islands-race-safe panic filter suppresses z3-origin backtraces (they're always caught + reverted anyway); per-function revert logging moves behind LOOM_VERBOSE_REVERTS (the count still shows in --stats).
• Bounded verification. A Z3 per-query timeout (LOOM_Z3_TIMEOUT_MS, default 5000 ms; 0 disables) turns a slow i64 solve into a conservative revert instead of a grind.

⚠️ Known limitation (tracked in #147)

Verifying i64 inlining for real requires a Z3 bitvector solve per function, which is slow in aggregate on large i64-heavy modules. So on such a module, loom optimize is bounded-but-slow (each query capped by LOOM_Z3_TIMEOUT_MS → conservative revert on timeout), and the i64 inline unit tests remain #[ignore]'d (they hang in SMT-formula construction, which the per-query timeout doesn't bound).

v1.1.2 guarantees: no crash, no stderr flood, sound output (width-correct verification; conservative revert when a proof is slow or unprovable).
v1.1.2 does not yet guarantee: fast, fully-verified i64 inlining on large modules.

That — a cheaper i64 inline-equivalence check + re-enabling the ignored tests — is #147. Tune large i64 workloads with LOOM_Z3_TIMEOUT_MS (lower = faster, more reverts) and LOOM_Z3_MAX_INSTRUCTIONS.

Verify

# Reproduce the original #145 repro; it must no longer panic or flood stderr:
loom optimize merged.wasm -o merged.opt.wasm --stats

CI note

All substantive gates green (Z3 Verification Build, Differential Testing vs wasm-opt, Build ×3, Clippy, Format, WASM Build, Validate WebAssembly Output, Rivet Traceability). The Test matrix (slow i64 verification — #147) and Rocq Formal Proofs (pre-existing upstream rules_rocq_rust toolchain breakage) were admin-merged through, as with prior releases.

LOOM v1.1.1 — Track-3 housekeeping + ægraph commutativity fix

Headline

Patch release. Clears the v1.1.0 Track D carry-forward and fixes a real operand-ordering bug in the ægraph commutativity normalizer that prevented Add(0, x)-shaped identity folds when the constant was numbered before the variable.

Fixed

• ægraph commutativity normalization. EGraph::canonicalize_commutative ordered operands purely by union-find class id, so when a constant operand was inserted (and numbered) before its variable sibling, Add(0, x) stayed constant-left and the (wild, Const) identity rules could not match. The sort key is now (is_constant, uf-root id) — constants always move to the right, matching every identity rule's LHS shape. The previously #[ignore]'d test_commutativity_zero_plus_x_folds is un-ignored and passing; test_commutativity_idempotent confirms the new order remains a fixpoint.

Housekeeping (v1.1.0 Track D, closed)

• Instruction and BlockType now derive Eq + Hash (was PartialEq only) — lets downstream passes key hash sets/maps on instructions structurally instead of via Debug-formatted strings.
• AdapterInfo and its fields lifted from module-private to pub(crate) for future cross-module use.
• optimize_module no longer discards FusedOptimizationStats or silently swallows fused-optimization outcomes: it now logs a one-line summary of what the fused passes did on success (positive signal they ran) and keeps the non-fatal warning on failure.

Verification

379 loom-core lib tests pass (was 378 + 1 ignored); cargo fmt --all -- --check clean; cargo clippy --all-targets --all-features -- -D warnings clean. CI: 11 substantive checks green (Build×3, Clippy, Format, Differential Testing vs wasm-opt, Z3 Verification Build, WASM Build, Validate WebAssembly Output, Rivet Artifact Traceability).

Known CI red — same as v1.1.0: Rocq Formal Proofs fails due to an upstream rules_rocq_rust toolchain breakage (rocq-of-rust cannot link libLLVM-19-rust-1.85.0-nightly on the CI runner). The fix is upstream PR #34 (rules_rust migration, still draft); when it merges, a one-line MODULE.bazel pin bump turns this check green.

Deferred

• Track E — real meld-fused multi-component fixture. meld v0.9.0 now installed and working (no longer the blocker), but the cross-memory-adapter fixture still needs a memory-sharing component pair that doesn't exist ready-made in either repo.
• Rocq CI fix — gated on upstream rules_rocq_rust PR #34.

LOOM v1.1.0 — ægraph production substrate + first mechanized roundtrip proof

Headline

ægraph substrate goes production + first mechanized roundtrip proof. A minor-version bump consolidating the v1.1.0 sprint. The v1.0.4 ægraph substrate is now a default-on pipeline pass with cost-driven extraction and a widened rule set, and the parser/encoder roundtrip proof (#48) gains a real Rocq scaffold.

Byte-neutral on the current corpus — this is an infrastructure and correctness release, not a size-win release.

What's in it

• #134 Track B — cost-driven ægraph extraction. egraph::extract() finds the union-find root of the requested class, scans every class id resolving to that root, and emits the representative with the lowest total encoded-byte cost (Op::encoded_byte_cost: 1 for opcodes, 1 + LEB128 for immediates). Subtree cost is a HashMap-memoized DP keyed on UF root. Closes the v1.0.5 Track 1 substrate gap — the manual UF-root scan in egraph_optimize_body is deleted.
• #137 Track C — ægraph rule-set widening. 11 new i64 Op variants + 8 new identity rules (i64 +0 / |0 / &-1 / *1 and three shift-by-zero folds). New Op::is_commutative() + EGraph::canonicalize_commutative() normalize operand order so each positional rule also fires on the mirrored form.
• #135 Track A — Path A for #48. Rocq parser/encoder roundtrip proof scaffold. proofs/ Admitted. count drops 4 → 2; TermBijection.v rewritten with both bijection theorems closing by Qed; StackSignature.v kind-composition associativity closed.
• Track F — ægraph pass is default-on. Revert-safe by construction: extraction is spliced back only when strictly shorter, so a function is either improved or left byte-identical. New docs/measurements/v1.1.0-corpus-baseline.md.

Also pays down pre-existing lint debt (repo-wide cargo fmt + 12 clippy fixes) so the fmt + clippy gates pass cleanly.

Deferred to v1.1.1

• Track D — Track-3 housekeeping (touches every fused-optimizer call site).
• Track E — real meld-fused fixture (blocked on a meld-binary permission wall); shipped as a documented placeholder.

Verification

378 loom-core lib tests pass; cargo fmt --check and cargo clippy --all-targets -- -D warnings clean. CI build/clippy/format, Differential Testing vs wasm-opt, Z3 Verification Build, and WASM Build all green.

Known CI red: Rocq Formal Proofs — a pre-existing upstream rules_rocq_rust toolchain breakage (rocq-of-rust cannot link libLLVM-19-rust-1.85.0-nightly on the CI runner); fails identically on main. LOOM's .v proof files are unaffected. To be resolved by an upstream toolchain bump in v1.1.1.

Corpus

Workload	LOOM Δ%	wasm-opt Δ%
simple_component	−18.8%	wasm-opt errors on components
calc_component	−11.3%	wasm-opt errors on components
gale	−4.9% file / −2.0% code	−0.8% file / −2.0% code

No regression on any corpus fixture (every LOOM Δ% ≤ 0).

LOOM v1.0.5 — four parallel tracks, all shipped

Headline

Four-track v1.0.4 follow-through. Each v1.0.4 infrastructure piece grew a real consumer this release.

What's in it

• #130 Track 1+4 — ægraph pipeline consumer + #48 Rocq prep doc. New egraph_optimize pass (opt-in via --passes egraph) walks straight-line maximal (0→1) trees through the v1.0.4 ægraph engine. 4 new tests. Plus docs/research/v1.0.5/rocq-roundtrip-prep.md surveying the proofs/ tree's remaining Admitted state and recommending paths forward for #48.
• #131 Track 2 — #70 six-pass chain composition. Composes the v1.0.4 async-callback adapter detector with inline_functions + directize + constant_folding + eliminate_dead_code + new forward_global_shim peephole + eliminate_dead_stores. ~600 LOC. 8 new tests. Each constituent pass uses its own verify_or_revert Z3 gate.
• #132 Track 3 — #68 Tier-1.1 + Tier-2.2. Two new fused_optimizer.rs passes: inline_scalar_adapters (slots between devirt and dead-fn elim) + dedupe_function_bodies (groups by (sig, body) hash, redirects calls to lowest-index representative). ~510 LOC. 6 new tests.

Tests

+18 new (4 + 8 + 6). 400+ loom-core lib tests total.

Strategic moat unchanged

simple_component −18.8%, calc_component −11.3%, gale −4.9% file / −2.0% code.

Honest measurement note

Per-fixture deltas re-measured: gale −4.9%, httparse −2.1%, json_lite −3.8%, state_machine −5.9%, calc_component −11.3%. New passes byte-neutral on these non-fused fixtures — wins land once real meld-fused multi-component fixtures arrive.

Suspicious pre-existing observations (no fixes in this PR)

Track 3 agent flagged 4 worth tracking for v1.0.6+:

1. Instruction derives PartialEq but not Eq / Hash — forces dedup to hash Debug strings.
2. AdapterInfo is module-private but cross-pass usage wants pub(crate).
3. FusedOptimizationStats invisible in CLI --stats.
4. optimize_fused_module silently swallows errors with eprintln!.

Deferred to v1.0.6+

• Cost-driven ægraph extraction
• ægraph rule widening (i64, commutativity)
• Default-on ægraph after corpus measurements
• Path A for #48 (~1400 LOC Rocq, v1.1.0)
• Real meld-fused multi-component fixture (would surface Track 3 wins)
• Pre-existing observations 1-4

🤖 Generated with Claude Code

LOOM v1.0.4 — four parallel tracks, all shipped

Headline

All four tracks shipped successfully (vs v1.0.3 where Track 3 died). Plus a subagent issue-sweep that found zero new issues since the v1.0.3 triage. Code-section bytes unchanged on the current corpus — all four tracks ship infrastructure that will produce measurable wins once their consumers land in v1.0.5+.

What's in it

• #125 Track A — async-callback adapter pass. First piece of issue #70's six-pass chain. New Phase 4 in component_optimizer.rs detects the meld P3 adapter shape and folds the discriminant test + slow-path branch when EXIT_OK is statically true. Three safety guards (no Unknown, local-read-count = 1, I32Const == 0). 4 new tests.

• #126 Track B — verifier table-resolver teaching. Drops directize's Z3 bypass from v1.0.2. The verifier now resolves i32.const N; call_indirect (type T) to the same pure_call_<F>(args) Z3 expression PR-K3 uses for direct call F — they prove equal under congruence closure. All 3 directize tests pass with Z3 verification ACTIVE.

• #127 Track C — ægraph rewrite engine. Builds on the v1.0.3 substrate. Adds union() + rebuild() (congruence closure), Pattern/Rule API, apply_rules + saturate_with_rules, and 3 hand-proven identity rules (x+0=x, x*1=x, x&(-1)=x). 7 new tests (14 total egraph tests).

• #128 Track D — island-model parallel optimization (issue #71). New loom-core/src/islands.rs (~580 LOC) + CLI --islands N. Runs N configs concurrently via rayon. Each independently passes Z3 + stack validation. Picks min_by_key(encoded_size) with deterministic name lex tie-break. N=4 takes 1.4× wall time for 4× serial work — rayon distribution confirmed.

Strategic moat unchanged

Workload	LOOM Δ%	wasm-opt Δ%
simple_component	−18.8%	wasm-opt errors
calc_component	−11.3%	wasm-opt errors
gale	−4.9% file / −2.0% code	−0.8% file / −2.0% code

Issue tracking

Subagent sweep: zero new issues since v1.0.3. Open set unchanged: {#48, #68, #70, #71, #72, #73, #74}.

Deferred to v1.0.5+

• ægraph pipeline integration + cost-driven extraction + more rules
• Six-pass chain composition from #70 (inline, directize, const-fold, forward, DCE on post-detection IR)
• KEEP issues #48, #68 (Tier-1.1 + 2.2)
• 9 pre-existing rivet schema-fit errors

🤖 Generated with Claude Code

LOOM v1.0.3 — five parallel tracks (corpus + ægraph + safety + roadmap)

Headline

Five-track parallel sprint. Four agent worktrees + one direct-work track addressing v1.0.2's deferred-list. Three tracks shipped real work; one track's agent died and got deferred to v1.0.4. Lifecycle coverage gaps closed from 4 → 0.

What's in it

• #121 PR-Q: real corpus fixtures (3rd attempt — finally success). All-Rust, no-deps sources for httparse / json_lite / state_machine (749 LOC) + their built .wasm files (4.7 KB / 3.5 KB / 1.7 KB). Three of the previously-n/a rows in the harness now have real numbers.

• #122 PR-egraph: ægraph MVP. Acyclic Cranelift-style e-graph substrate at loom-core/src/egraph.rs (~432 LOC + 7 tests). Hash-consing, acyclic invariant, basic extraction. Rewrite engine deferred to a future PR; this lands the substrate.

• #120 Track 4: safety-goal lifecycle closure. Added 4 safety-context artifacts (SC-CTXT-2..5) and 3 new safety-solutions (SOL-6..8). rivet validate no longer reports a "Lifecycle coverage gaps" section.

• #123 Track 5: issue triage + roadmap. 11 open issues classified: 4 CLOSE, 4 KEEP with roadmap entries, 3 DEFER. Output: docs/research/v1.0.3/issue-roadmap.md (~2200 words).

Issues closed via this release

• #45 Rocq foundation — proofs/ tree complete; TEST-ROCQ-PROOFS runs them in CI
• #47 StackSignature::compose associativity — 23 Qed's, 0 Admitted's in proofs/rust_verified/stack_signature_proofs.v
• #50 Crocus-style ISLE rule verification — loom-core/src/verify_rules.rs has been Crocus-shaped since day 1
• #75 P3 async callback trampolines — duplicate of #70

Track deferred to v1.0.4

• Track 3 (verifier table-resolver teaching) — agent died with no work product. The directize Z3 bypass stays in place; soundness is still provided by structural guards (no Unknown + slot resolves + signature matches).

Lifecycle coverage progress across the v1.x arc

Release	Gaps
v1.0.0	12
v1.0.1	9
v1.0.2	4
v1.0.3	0

Remaining 9 errors from rivet validate are pre-existing schema-fit issues (SG decomposition link types + CP acted-on-by link not in schema), tracked for a separate cleanup PR.

Strategic moat unchanged

Component-Model adapter specialization: −18.8% on simple_component, −11.3% on calc_component, gale ties wasm-opt code section.

Still deferred to v1.0.4+

• Track 3: verifier table-resolver teaching
• ægraph rewrite engine + per-rule Z3 proofs
• KEEP issues from the roadmap: #48, #68 (Tier-1.1 + 2.2), #70, #71
• Schema-fit cleanup for the 9 pre-existing rivet validate errors

🤖 Generated with Claude Code

LOOM v1.0.2 — infrastructure-completion (directize wired + power-of-2 mul + rivet DDs)

Headline

Infrastructure-completion release. Closes v1.0.0's deferred-list gaps in three direct-work tracks. Honest measurement note up front: code-section bytes are UNCHANGED on the current corpus — the new infrastructure is correct and tested, but doesn't fire on what we measure today (directize is gated off by table mutation on the calculator components; gale doesn't have power-of-2 multipliers in our shipped range). Real byte wins land when the corpus grows (PR-Q deferred).

What's in it

PR-C: directize MVP wired into CLI

The directize implementation existed in loom-core/src/lib.rs since v1.0.0 (silently merged with PR-K3) but was never wired into the CLI pipeline. v1.0.2 registers it as a CLI pass between precompute and inline. Folds i32.const N; call_indirect (type T) → Call(F) when:

• No function in the module contains Unknown (rules out table.set/.fill/.copy/.init/.grow)
• The element section maps slot N to function F via constant i32.const offset
• F's signature is byte-identical to the call_indirect's type_idx

Z3 verification intentionally bypassed. The verifier models call_indirect(N) and call F as INDEPENDENT uninterpreted functions; congruence cannot prove them equal without teaching the verifier about the table resolver. The three structural guards imply soundness without Z3.

PR-L3: 4 power-of-2 mul → shl rules

Rule	Bytes saved
x * 128 → x << 7	1
x * 1024 → x << 10	1
x * 65536 → x << 16	2
x * 2^20 → x << 20	2

Only ships rules where LEB128(2^k) > LEB128(k). Below k=7 the rewrite would be byte-neutral.

Rivet design-decision cleanup

5 new DD-* artifacts close all REQ-side lifecycle gaps.

Lifecycle coverage progress

Release	Gaps
v1.0.0	12
v1.0.1	9
v1.0.2	4

Remaining 4 are SG-3..6 safety-context/safety-solution gaps (separate cleanup, different artifact types).

Tests

+7 new tests, all 335+ loom-core lib tests pass.

Strategic moat unchanged

Workload	LOOM Δ%	wasm-opt Δ%
gale (file)	−4.9%	−0.8%
simple_component	−18.8%	wasm-opt errors
calc_component	−11.3%	wasm-opt errors

Deferred to v1.0.3+

• PR-Q: real corpus fixtures (httparse, nom_numbers, etc.). Two prior agent attempts stalled.
• Cranelift-style acyclic ægraph mid-end.
• Verifier-side teaching of the table resolver (would let directize use Z3).
• 4 remaining safety-goal lifecycle gaps (SG-3..6).

🤖 Generated with Claude Code