perf: precisely short-circuit exact forwarders (fmodf et al. libm calls) and zero-forwarders (Motoko-specific)

[ggreif]

Summary

Short-circuit two classes of Wasm call-indirection in the linker, before RTS imports are resolved:

• Exact forwarders (libm/RTS side). forwarding_target in src/linking/linkModule.ml detects functions whose body is local.get 0 … local.get n-1; call k — the Rust #[no_mangle] wrappers for fmod, fmodf, pow, sin, cos, …. chase_forwarders rewrites the RTS exports map so each export resolves directly to its terminal callee, bypassing the wrapper. The moc-generated call site then hits $libm::… directly.

• Zero-forwarders (Motoko-specific). zero_forwarder_target detects Motoko top-level functions whose body is i{32|64}.const 0; local.get 1 … local.get n-1; call k — they forward all arguments through, passing a zero as the closure slot. A new abstract interpreter (src/linking/constTrack.ml{,.mli}, ~495 lines) propagates integer constants over the Wasm operand stack: straight-line code, Block/Loop/If join points, Br/BrIf/BrTable, Select, Compare/Test, Unary/Convert, with local-tracking and FromLocal backprop. At each Call k where k is a 0-forwarder and the closure arg on the stack is i{32|64}.const 0 specifically, the call is rewritten to the chain's terminal. A nonzero constant is deliberately rejected: the forwarder would have overwritten the closure with zero, so eliding it would leak the caller's value to a callee that may inspect $clos.

Forwarder-chain compression (termination + cycle safety)

Both forwarder maps (chase_forwarders on RTS exports and the 0-forwarder map on em1 locals) are compressed via Kleene pointer-jumping with a difference-map output: each step expands every entry's target via the current map; iteration terminates when the diff is empty, or a fuel bound of cardinal raw kicks in (guarding against odd-length cycles where pointer-jumping oscillates rather than converges). A post-filter drops any entry whose compressed target is still a key of the converged map — those sit on or lead into a cycle and have no well-defined terminal. With the map compressed and cycle-free, the call-site rewriter needs one pass and cannot loop.

Nested-block-safe rewrite via physical identity

ConstTrack.process_block_inner recurses into Block/Loop/If bodies with a fresh idx=0, so positional keys would mis-target calls inside nested blocks. Rewrites are therefore keyed on the physical identity of the instr phrase (ConstTrack.same_instr, backed by OCaml ==). Apply walks the body recursively, descending into the three nested forms. Sound under the linker's tree-shaped IR invariant (no phrase sharing, no position aliasing); documented in constTrack.mli.

constTrack.mli is a public interface — the abstract interpreter is reusable by future linker passes.

Tests

test/run/fmodf-forward.mo (FileCheck, classical + EOP + wasm64):

• fmodf call site reaches $libm::…fmodf… directly.
• Motoko foo → bar → quux chain collapses: foo calls quux directly (bar is a 0-forwarder).
• baz (which adds 1.0 after calling quux) is not collapsed — not a pure forwarder.
• Unreferenced $fmodf wrapper remains in the binary (to be DCE'd by wasm-opt).

test/run-drun/blob-dedup-upgrade.drun under --sanity-checks --enhanced-orthogonal-persistence — this was the regression that motivated the nested-block fix. The sanity-check instrumentation introduces nested Blocks around calls; without physical-identity keying, the rewriter landed on the wrong instruction and produced expected [i64, i64] but got [i64] at load time.

test/run.sh — small portability fixes for macOS 26.4 (tr -d '\000', paste -sd' ' -).

Follow-up

PR #5964 is stacked on this one and handles the case chase_forwarders cannot: call_indirect for capturing closures (foo_clos → bar.1 → quux.1) where the function index is statically known but the closure carries a captured value.

Design notes

• .claude/plans/abstract-interpreter.md
• .claude/plans/call-forwarding.md
• .claude/plans/wasm-exts-update.md

Test plan

• make -C test/run fmodf-forward.only — [tc] [run] [comp] [valid] [FileCheck] [wasm-run] pass (classical, EOP, wasm64).
• make -C test/run-drun blob-dedup-upgrade.only under --sanity-checks --enhanced-orthogonal-persistence — passes.
• make -C test/run -j10 quick — all tests pass.

🤖 Generated with Claude Code

[github-actions]

Comparing from bc32e40 to edade2b:
In terms of gas, 5 tests improved and the mean change is -0.5%.
In terms of size, 5 tests regressed and the mean change is +0.0%.

[ggreif]

Instruction count reduced: 5_522_892_825 → 5_405_452_313 (−1.1%)

[ggreif]

Instruction count reduced: 1_153_792_735 → 1_153_792_714 (−21 instrs)

[ggreif]

too convoluted

[ggreif]

This is AI-written, needs rewrite to make it nicer.

[ggreif]

I think this is a lie. We need a strict guarantee that const 0 is at the exact right stack depth. See section "Precise call-site eligibility via stack-depth tracking" below!

[ggreif]

Agreed — the Safety paragraph is loose. "Any i32.const k before the call" isn't enough; the const has to be the value on the operand stack at depth n-1 (0-indexed from TOS, with n = callee arity) at the instant the call executes. That is exactly what the "Precise call-site eligibility via stack-depth tracking" section below describes, and what the shipped code checks at each call site via ConstTrack.lookup state (n-1) in the on_call callback.

I'll tighten this subsection so it points at the stack-depth criterion rather than implying a textual/peephole match, and remove the "any i32.const k" framing.

[ggreif]

Turned out there was a second, independent bug of the same spirit: the shipped on_call predicate in linkModule.ml (line 1113) matched any ConstTrack.I32 _ | I64 _ at the closure-arg depth, not zero specifically — a regression from 80ae9b7 when the flat-array heuristic (which had I32 0l | I64 0L) was replaced by the abstract interpreter.

A nonzero caller constant would have reached the terminal $k unchanged after elision, which is unsafe if $k inspects $clos (not a linker-provable invariant for an arbitrary callee). Tightened the predicate to Some (ConstTrack.I32 0l | ConstTrack.I64 0L) and rewrote the Safety subsection to match. b87813a.

Tests still pass because moc only emits i32.const 0 for top-level named calls — but the previous code was one malicious caller away from producing wrong Wasm.

[ggreif]

The callee might examine the passed in closure and use it when not zero. So short circuiting is only permissible when the call-site really passes a zero.

[ggreif]

Independent review summary (soundness pass)

Dispatched an independent review agent over the three fix commits (b87813adb, e98cfeccb, 8e2f8dc8e, plus the follow-up refactor 8a999ffec). Gist of its findings:

Sound — nothing wrong

• Zero-specific closure predicate (b87813adb): tight. The forwarder overwrites $clos with 0 before calling its callee; only a caller-supplied 0 preserves semantics at the terminal's entry. Matching I32 0l | I64 0L is correct; "any i32.const k" would leak nonzero values to a callee that may inspect $clos.

• Path compression with fuel + cycle drop (e98cfeccb): termination verified explicitly for length-2 and length-3 cycles. Length-2 collapses to self-loops in one step (both still in dom(m')); length-3 oscillates permutationally with period 3, so by k=cardinal all cycle entries still point into dom(m'). The post-filter not (Int32Map.mem t m') correctly drops both cyclic nodes and tail nodes leading into a cycle, since after Kleene convergence any non-terminal-reaching entry still has m'[fi] ∈ dom(m').

• Physical-identity rewrite (8e2f8dc8e, refactored in 8a999ffec): the reasoning is right — process_block_inner recurses with fresh idx=0, so a positional key would collide across nesting levels. Since moc's IR is tree-shaped (no phrase sharing), == is a correct key. The rewrite_instr descent mirrors the three recursive cases in ConstTrack.step.

Fragile — flagged, not errors

• Fuel bound cardinal raw is conservative; ⌈log₂ cardinal⌉ would be tighter. Non-issue at the expected scale (<100 entries).
• == soundness depends on the non-local "no phrase sharing" invariant. Now documented via ConstTrack.same_instr so any future optimisation that introduces memoisation of phrases would trip over the documented assumption.
• on_call doesn't re-check n_params ≥ 1; safe today via zero_forwarder_target's own guard at linkModule.ml:234, but the coupling is implicit.
• Cross-width closures (i32/i64 mix under the wasm64 transition) — safe provided type-checking agrees on width, which upstream enforces.

Alternatives considered, not taken

• Tarjan SCC for exact cycle detection — more defensible than fuel, but fuel is cheaper and sufficient here.
• Pushing nested-block awareness into ConstTrack's API (e.g., absolute-path key) — addressed instead by exposing ConstTrack.same_instr as a named helper so the identity invariant is documented in one place.
• chase_forwarders (dm2/RTS exports) and the em1 rewriter operate on disjoint function arrays and disjoint maps; ordering is independent.

Bottom line

No correctness issues found across the four commits.

[ggreif]

Phase 3 (constTrack) just landed on this branch

Three commits implement the precise branch-join design sketched in .claude/plans/abstract-interpreter.md § "Phase 3: Precise branch joins via algebraic effects", plus a fourth with a linker-level regression test:

• 7d815c4d1 feat(constTrack): Phase 3 — precise branch joins via algebraic effects
• 14c04cd6b refactor(constTrack): extract run_under_leave_handler + join_branch_states
• e96295b56 test(ld): zero-forwarder regression test exercising Phase 3 precision
• c58d0f6f6 test(ld): expand zero-fwd-join to 4 Phase-3 regression cases

Review-agent verdict

An independent reviewer with an effects / SSA / Wasm brief walked the two constTrack commits, traced two nested cases step-by-step (Block { Block { If { Br 2 } } } and Block { Loop { Br 1 } }) through the handler chain, and reported:

• No correctness bugs. Effect semantics hold: Effect.perform inside an effc function re-dispatches to the next outer handler (OCaml 5.3 built-in), so the de-Bruijn decrement chain (n → n-1 → ... → 0) works as intended. Every handler invokes continue k () exactly once per branch; no continuation is dropped or double-invoked.
• No soundness regression vs Phase 2. Every scenario considered is at least as precise as Phase 2 and strictly better in three: (1) no-BrIf blocks preserve constants the has_br_if hack left alone; (2) BrIf-taken and fall-through paths that agree on a result slot now retain the constant where Phase 2 bulk-evicted; (3) unconditional Br 0 in a Block now joins only the Br-taken LRU, where Phase 2 cleared entries. BrIf's sense=false refinement remains applied to fall-through only — semantically correct and unchanged.
• Refactor is behaviour-preserving. The three inlined handlers had identical n>0 re-raise arms; extracting run_under_leave_handler changes nothing semantically. The shared branch_states ref across If's two legs works because the two run calls evaluate sequentially; join_branch_states is order-independent (intersect is commutative/associative). normalise:false + swallowing on_zero recovers the Loop variant verbatim.

Regression detector

The reviewer's four suggested test cases live in test/ld/zero-fwd-join.wat as four exported call sites:

Reviewer's example	Function name in test
Nested-Block de-Bruijn depth	$nested_block
Block { Loop { Br 1 } }	$block_over_loop
Agreeing BrIf (canonical)	$agreeing_brif
If with agreeing legs	$agreeing_if_legs

Each function ends with call $bar where $bar is a syntactic zero-forwarder (body: i32.const 0; local.get 1; call $quux). Phase 3 sees the i32.const 0 at depth n_params - 1 through each pattern and lets collect_rewrites rewrite every call $bar → call $quux. Verified by temporarily reverting constTrack.ml to the pre-Phase-3 commit: all four call sites regress to call $bar (unrewritten), producing a four-way diff against the committed .ok. Under Phase 3 the .ok matches verbatim.

Still unblocked from the plan doc

Phase 3 was gated on "OCaml 5.3 migration (draft PR exists)" — that's now f1e676ae0 on master. This branch merged master in 7771c1f9a, so Phase 3 could finally land. Any future revert of Phase 3 is caught by the test/ld/zero-fwd-join diff.

[ggreif]

Follow-up — BrTable now modelled

The earlier comment left BrTable _ -> None as "not yet modelled". Just pushed 6f2d94c2d feat(constTrack): model BrTable + 5th regression case that plugs the gap:

| BrTable (targets, default) ->
  let lru = shift_and_evict (-1) lru in  (* pop the index *)
  List.iter
    (fun t -> May_leave (label_depth t, lru) |> Effect.perform)
    (targets @ [default]);
  None

Each target — listed plus default — receives one May_leave carrying the popped-state LRU. The enclosing handler chain does the de-Bruijn decrement exactly as for Br/BrIf.

5th regression case in test/ld/zero-fwd-join.wat: $br_table_agree

(func $br_table_agree (type $t_i)
  (block (result i32)
    i32.const 0
    local.get 0
    br_table 0 0 0 0        ;; three listed + default, all target this block
  )
  local.get 0
  call $bar)

Every target contributes [d0 = I32 0] to the Block's branch_states; the fold-intersect keeps 0; the linker rewrites call $bar → call $quux.

Verified as a strict regression detector by temporarily reverting only the BrTable arm of the step function while keeping the rest of Phase 3 intact: the diff shows exactly one call $quux → call $bar regression (the new 5th function); the other four cases remain rewritten. So this commit is load-bearing just for the BrTable precision, independent of the earlier Phase 3 work.

Review-agent verdict (focused pass on the BrTable arm)

A follow-up review across five angles — Wasm semantics, per-target stack shape, duplicate targets, de-Bruijn chain through disjoint-depth targets, and the None-terminator/iteration-order details — came back with no bugs found:

• Wasm semantics match: shift_and_evict (-1) pops the index; each possible successor gets the same post-pop state. No index-range reasoning needed — out-of-range → default is already covered by the list iteration, and must-converge intersect is over-approximating by construction (contributing to every syntactically-reachable target is sound since runtime picks exactly one).
• Homogeneous stack shape: Wasm validation forces identical label arity across all targets + default, so sending the same lru to every target cannot produce a type-shape mismatch at the intersect site.
• Duplicate targets harmless: intersect is idempotent on equal inputs; the 5th test's br_table 0 0 0 0 proves this end-to-end.
• Disjoint-depth trace: walked block_outer { block_mid { block_inner { br_table 0 1 2 } } } explicitly — block_inner catches the depth-0 contribution directly; the depth-1 re-raises through block_inner to block_mid; the depth-2 re-raises through block_inner and block_mid to block_outer. Each enclosing Block receives exactly one contribution at its own level.
• None return + targets @ [default] ordering: both correct; intersect is commutative/associative so concat order is immaterial; the top-level process_block handler swallows any May_leave escaping from a function-scope br_table.

Verdict reproduced verbatim: "sound, complete for the control-flow lattice, and consistent with the Br/BrIf arms. Arguably the minimal correct implementation given the existing Phase 3 framework."

Updated case table

Reviewer example	Function name
Nested-Block de-Bruijn depth	$nested_block
Block { Loop { Br 1 } }	$block_over_loop
Agreeing BrIf (canonical)	$agreeing_brif
If with agreeing legs	$agreeing_if_legs
BrTable, all targets agree	$br_table_agree

All five call sites get rewritten under Phase 3 + BrTable; each regresses to call $bar when the corresponding feature is reverted.