opt: dissolve the seam fully — post-inline SROA/scalar-forwarding eliminates the u64 ABI pack/unpack (+ wasm-local mem2reg) → toward LLVM-LTO parity

[avrabe]

Context: loom currently --passes inline dissolves the gale C↔Rust decide seam into the kernel-primitive shims (sem/mutex/pipe/…). It inlines the call but doesn't yet dissolve the seam — the decide's u64-packed-return ABI survives the inline as a pack-immediately-unpack round-trip. This is the bulk of our gap vs LLVM-LTO (sem handoff: 860 cyc wasm-cross-LTO vs 471 LLVM-LTO = 1.83×; G474RE silicon).

Evidence (wasm-IR, post-loom-inline — frozen repro attached)

repro-loom-seam-sroa/sem.loom.wasm (the dissolved z_impl_k_sem_give) still contains, on the same value:

i64.extend_i32_u ; i64.shl ; i64.or     ← decide PACKS {action, new_count} into a u64
...
i64.and ; i64.shr_u                      ← shim UNPACKS it back to scalars
(local i32 i32 i64)                      ← the dead i64 carrier local

The u64 is constructed from two i32s and immediately decomposed — textbook SROA / scalar-forwarding. LLVM-LTO sees through this and it vanishes; we keep it.

Cost it produces (synth ARM backend, z_impl_k_sem_give = 83 insns / 540 B object)

• u64 round-trip: str.w r0,[sp,#0x8]; str.w r1,[sp,#0xc] (spill the packed halves) then and.w r4,r0,#0xff (unpack action) — pure ABI residue.
• wasm-local reload churn: 19/83 insns (23%) are [sp] traffic; the pointer arg is reloaded 5× from [sp,#0x68] (each local.get → memory).
• const re-materialization: 11 movw/movt (the 0xff/0x1 unpack masks + linmem base, not hoisted).

Recommended passes (all wasm-IR → benefit ARM and RISC-V backends; complementary to synth#209's backend regalloc)

1. SROA / scalar-forwarding through the inlined seam (highest value) — when an i64 is built by extend/shl/or and consumed by and/shr_u with no escape, forward the scalar components directly and drop the carrier local. Kills the pack/unpack outright. This is what turns "inlined" into "dissolved."
2. wasm-local mem2reg / promotion + coalescing — promote non-escaping single-assignment locals and shrink the live set so the 5× pointer reload + store-then-reload chains collapse to register keeps.
3. const dedup / hoisting — materialize each constant once (also addresses the documented 61% const-redundancy in flat_flight).

Parity read

Bit-exact 1.0× vs LLVM-LTO is unlikely (their regalloc is decades-tuned), but within ~20% is achievable, and the in-context overhead is already +11% (composed flight_control bench). Levers 1+2 alone should take the sem body from 83 insns toward ~55–60 (drop the u64 round-trip + most [sp] churn) — a large chunk of the 1.83×.

Kill-criterion

On a build with pass #1: repro-loom-seam-sroa/sem.loom.wasm → synth shows no i64 pack/unpack in the dissolved body, the i64 local is gone, and the ARM body drops below ~70 insns. I'm the on-silicon gate (G474RE) — I'll re-measure sem 860 + mutex 472 + the composed-bench deltas the moment a build lands.

Repro: gale-smart-data/.../wasm-testbed/repro-loom-seam-sroa/ (sem.loom.wasm + shim). xref synth#209 (backend regalloc/const-CSE — the complementary lever).

[avrabe]

Phase 2 — the goal is to BEAT the status quo, not just reach LLVM-LTO parity. Phase 1 above (SROA-through-inline + mem2reg + const-dedup) closes the gap to ~parity. The structural advantages of the dissolve-at-wasm-IR path mean we can go past native/LLVM-LTO:

1. Cross-language whole-program specialization (beats both) — at the dissolved wasm-IR, the C kernel hot path and the verified-Rust decide are one uniform module. LLVM-LTO LTOs within a language/codegen-unit; native-C can't see the Rust decide at all. loom can specialize the decide to call-site constants (e.g. a k_sem with a compile-time-known limit, a fixed msg_size) and propagate across the seam in ways neither alternative can. That's a structural edge, not a tuning knob.
2. Hot/cold layout from the decision structure — the decides encode the fast path (no-waiter give, uncontended unlock) vs the cold wake/pend path. Lay the fast path straight-line, sink the cold arm out-of-line. Native relies on hand __builtin_expect; we have the whole decision graph.
3. Verified ⇒ guard-elision (the security-makes-it-FASTER lever) (research, needs per-primitive audit) — the decides are Verus/Kani/Rocq-proven. Where a precondition is proven to hold, the corresponding defensive runtime guard in equivalent C is provably redundant and can be elided. So the verified path can be faster than defensive C precisely because it's verified — the deepest form of "security and speed are not a tradeoff." Needs an audit of which dissolved-body guards are proof-backed-elidable.

The pitch this enables: today's RTOS kernels run unverified hand-C decision logic. gale runs formally-verified Rust that dissolves to native-equal-or-better code, behind a capability-typed WIT component boundary (gale#63). Neither native-C (fast, unverified) nor a sandboxed wasm interpreter (safe, slow) gets both — this path is the only one that does. Functionality is already proven on real silicon (full primitive surface + composed flight_control bench, no fault); we're past "make it run" and into "make it win."

I'm the on-silicon gate (G474RE) for all of this — each lever gets a before/after on hardware.

[avrabe]

Picking this up — it's the right next step: turning "inlined" into "dissolved." Confirming the design so we're aligned before I land code.

Plan (provably-correct, staged)

The round-trip is pack (build i64 from two i32s via extend_i32_u/shl/or) → store to a carrier local → unpack (and/shr_u → wrap_i64). Dissolving it needs three cooperating pieces:

1. Single-assignment carrier promotion (wasm-local mem2reg). Promote the non-escaping, single-assignment i64 carrier so each local.get $t at an unpack site is replaced by the pack expression itself. This is what exposes the algebra; without it the pack/unpack are separated by local.set/local.get and never meet.
2. Pack/unpack algebraic forwarding (SROA, pass Phase 1: Project Setup and Build Systems #1). With the pack expression in hand at the unpack site, apply the bitwise identities:
   • (extend_u(a) | (extend_u(b) << k)) & mask → a when mask selects exactly a's bits and a's width ≤ k.
   • (... ) >> k then mask → b. Then wrap_i64 of an extend_i32_u(x) → x.
     Each identity gets a Z3 proof before it's enabled — no rule ships without its soundness obligation discharged. The carrier and pack go dead and DCE removes them.
3. const dedup/hoist — folded in after, addresses the 61% const-redundancy too.

i64.extend_i32_u/i32.wrap_i64 aren't ISLE terms today, so step 2 either adds those term types (preferred — keeps it in the proven ISLE layer) or runs as an instruction-level pass with the same Z3 obligations.

Two asks

• Repro access: I don't have gale-smart-data/.../repro-loom-seam-sroa/sem.loom.wasm on my side. I'll build a faithful local WAT fixture of the exact pack/unpack shape to develop+prove against, but if you can attach sem.loom.wasm to this issue I'll validate against the real dissolved body directly.
• Heads-up: repo CI/release is currently stalled (GitHub Actions hasn't started a new run since ~06:42 UTC — the smithy self-hosted runners look offline), so the eventual release will need that back. Unrelated to this work; flagging so the "build lands" timing is clear.

I'm the on-silicon gate is you (G474RE) — I'll get pass #1 to the kill-criterion (no i64 pack/unpack in the dissolved body, carrier local gone) and ping for the sem 860 / mutex 472 re-measure.

[avrabe]

Repro attached + design confirmed — go.

Your 3-piece plan is exactly right, and the Z3 obligation per ISLE rewrite is the part I'd have insisted on: it makes this proof-carrying optimization (no rewrite ships without its soundness discharged) — which is the same ethos as the verified decides it's optimizing. Preferring the ISLE-term route (adding extend_i32_u/wrap_i64 terms) over an instruction-level pass is the right call for keeping it in the proven layer.

Kill-criterion (on-silicon gate = me, G474RE):

• structural: dissolved z_impl_k_sem_give body has no i64 pack/unpack, the carrier local is gone, ARM body drops from 83 insns toward ~55–60.
• silicon: re-measure vs the locked baselines — sem 860, mutex 472 (and the composed flight_control bench in-context deltas: t_lock +82%, handoff +21%). I'll reflash the moment a build lands.

Repro — sem.loom.wasm (the exact dissolved body, post-loom-inline; sha256 f81da42d…33b032, 5254 B). Also committed at gale-smart-data/benches/engine_control/silicon/wasm-testbed/repro-loom-seam-sroa/ (+ the shim). base64 inline so you can validate against the real body directly:

sem.loom.wasm (base64)

AGFzbQEAAAABHwZgAX8Bf2ACf38AYAF/AGACf38Bf2AAAGADf39/AX4CegUDZW52C2tfc3Bpbl9sb2NrAAADZW52FXpfdW5wZW5kX2ZpcnN0X3RocmVhZAAAA2VudhxhcmNoX3RocmVhZF9yZXR1cm5fdmFsdWVfc2V0AAEDZW52DnpfcmVhZHlfdGhyZWFkAAIDZW52DHpfcmVzY2hlZHVsZQADAwUEBAUEAgQFAXABAQEFAwEAAgYIAX8BQYCABAsHNwMGbWVtb3J5AgAWZ2FsZV9rX3NlbV9naXZlX2RlY2lkZQAGEXpfaW1wbF9rX3NlbV9naXZlAAgKrwEEBQAQBwALSQEBfkIBIQMCQAJAAkBBAEEBQQIgACABSRsgAhsOAwIAAQILAkAgAEF/Rg0AIABBAWohAAwBCxAFAAtCACEDCyAArUIghiADhAsHAANADAALC1UCAn8BfkGAgAQQACEBIAAQASECAkACQCAAKAIIIAAoAgwgAkEARxAGIgNC/wGDQgFSDQAgAkEAEAIgAhADDAELIAAgA0IgiD4CCAtBgIAEIAEQBBoLAIACDS5kZWJ1Z19hYmJyZXYBEQElDhMFAw4QFxsOEQESBgAAAjkBAw4AAAMuAREBEgZAGAMOOgs7BT8ZAAAEHQExEBEBEgZYC1kFVwsAAAUdATEQEQESBlgLWQtXCwAABh0AMRARARIGWAtZC1cLAAAHHQExEFUXWAtZC1cLAAAIHQAxEFUXWAtZC1cLAAAJEQElDhMFAw4QFxsOAAAKLgBuDgMOOgs7CyALAAALLgBuDgMOOgs7BT8ZIAsAAAwuAG4OAw46CzsFIAsAAAABEQElDhMFAw4QFxsOEQFVFwAAAjkBAw4AAAMuABEBEgZAGG4OAw46CzsLNgs/GYcBGQAAAACyBwsuZGVidWdfaW5mb8gBAAAEAAAAAAAEAa4HAAAcAOcFAAAAAAAAGAcAAP////9uAAAAApYAAAACcAAAAALVAAAAAnsGAAAD/////24AAAAH7QMAAAAAn3sGAAAB3gEEQQIAAP////9gAAAAAeABKQU0AgAA/////2AAAAAFbQsFCgIAAP////8VAAAABRAhBv4BAAD/////CwAAAAJMOAb+AQAA/////wEAAAACTBoGnAIAAP////8JAAAAAkwnAAYcAgAA/////wEAAAAFETcFCgIAAP////8NAAAABREhBpwCAAD/////DQAAAAJMJwAGHAIAAP////8BAAAABRIcBQoCAAD/////AwAAAAUSIQacAgAA/////wMAAAACTCcAB2kCAAAAAAAABRcOCLwCAAAAAAAABowNAAckAwAAGAAAAAUVEwj/AgAAGAAAAAITCQAHaQIAADAAAAAFGg4IvAIAADAAAAAGjA0ABXsCAAD/////BQAAAAUZIQapAgAA/////wUAAAAGkA0ABXsCAAD/////BQAAAAUaJQapAgAA/////wUAAAAGkA0ABQoCAAD/////BwAAAAUTIQacAgAA/////wcAAAACTCcAAAAAAAAAAAD9AAAABAAAAAAABAmuBwAAHABTBQAAzwEAABgHAAAClgAAAAJwAAAAAosAAAACEwAAAAqEAgAArgAAAAFIAQqMBAAAvQAAAAFLAQACAAAAAArmAgAA3QAAAAE3AQAAAtUAAAAC2QAAAAoCAgAAOAUAAAIHAQAL1AMAAHsGAAAD1QEBAAAC5QAAAALgAAAAAmgAAAAChwAAAAIJAAAACoUBAAD5AAAABYsBAAI5AAAAChAEAADMAAAABY8BAAAAAAAAAvQAAAACuQAAAAImAAAADPIEAADMAAAABHwIAQzyBAAAzAAAAAR8CAEAAh0AAAAMPQIAAPkAAAAENAgBAAAAAGQAAAAEAAAAAAAECa4HAAAcAIQGAAAAAwAAGAcAAAL0AAAAApIAAAACgwAAAAIvAAAADD8DAACoAAAAARoBAQAAAAAClgAAAAJwAAAAAosAAAACdAAAAAqNAwAAQgUAAAISAQAAAAAAbQAAAAQAvQAAAAQBrgcAABwASAcAAH4DAAAYBwAAAAAAAEgAAAAC9AAAAALqAAAAA1oAAAAHAAAAB+0DAAAAAJ9UAQAAeQAAAAE8AwJcAAAAAwIAAAAJAAAAB+0DAAAAAJ8GAQAAQwAAAAGtAwAAAAAAbg0uZGVidWdfcmFuZ2VzNAAAADoAAABHAAAAVgAAAAAAAAAAAAAAOgAAADsAAABWAAAAXgAAAAAAAAAAAAAAOwAAAEAAAABoAAAAbQAAAAAAAAAAAAAAWgAAAGEAAAACAAAACwAAAAAAAAAAAAAAAPIPCi5kZWJ1Z19zdHJ7aW1wbCM2fQB7aW1wbCMyNH0Ae2ltcGwjMTR9AHtpbXBsIzR9AHtpbXBsIzN9AHtpbXBsIzkxfQB7aW1wbCMyMH0AcGFuaWNfY29uc3RfYWRkX292ZXJmbG93AHBhbmljX2NvbnN0AHN1cHBvcnQAaW50AERJbnQAcGFuaWNfZm10AGJpdABpbnRfdHJhaXRzAG9wcwBjb21waWxlcl9idWlsdGlucwBiaXRvcgB6ZXJvX3dpZGVuAG51bQB6ZXJvX3dpZGVuX211bAB3cmFwcGluZ19tdWwATXVsAGhpAGxpYm1fbWF0aABwYW5pY2tpbmcAY29yZQB3cmFwcGluZ19hZGQAX1pONGNvcmU5cGFuaWNraW5nMTFwYW5pY19jb25zdDI0cGFuaWNfY29uc3RfYWRkX292ZXJmbG93MTdoYWNlYzk2NmRmMjMwYTc4ZkUAX1pONGNvcmU5cGFuaWNraW5nOXBhbmljX2ZtdDE3aDY2NTEzMTNjM2UyYzZjMmZFAF9aTjg1XyRMVCRpMTI4JHUyMCRhcyR1MjAkY29tcGlsZXJfYnVpbHRpbnMuLm1hdGguLmxpYm1fbWF0aC4uc3VwcG9ydC4uaW50X3RyYWl0cy4uSW50JEdUJDEyd3JhcHBpbmdfYWRkMTdoNmVhZThmZmM4YTJhOTcyZkUAX1pOMTdjb21waWxlcl9idWlsdGluczNpbnQzbXVsM011bDNtdWwxN2hiMjQ3Yjk5MjZjODE4ZDNlRQBfWk40Y29yZTNudW0yMl8kTFQkaW1wbCR1MjAkaTEyOCRHVCQxMndyYXBwaW5nX2FkZDE3aDM5ZTBlZDJhYzU5ZWE2NmRFAF9aTjYwXyRMVCRpMzIkdTIwJGFzJHUyMCRjb21waWxlcl9idWlsdGlucy4uaW50Li50cmFpdHMuLkhJbnQkR1QkMTB6ZXJvX3dpZGVuMTdoYTQwZTIwNzAyNTQ5MGQ0ZEUAX1pONjBfJExUJGk2NCR1MjAkYXMkdTIwJGNvbXBpbGVyX2J1aWx0aW5zLi5pbnQuLnRyYWl0cy4uREludCRHVCQyaGkxN2hkZDEzMjA0NjM0ZmZmMDVjRQBfWk40Nl8kTFQkaTEyOCR1MjAkYXMkdTIwJGNvcmUuLm9wcy4uYml0Li5CaXRPciRHVCQ1Yml0b3IxN2hhMzkwZTk2NGRkZTQxNGE4RQBfWk4xN2NvbXBpbGVyX2J1aWx0aW5zM2ludDZ0cmFpdHM0REludDEwZnJvbV9sb19oaTE3aGUzN2MwYWU4MTUyOGMzYzdFAF9aTjE3Y29tcGlsZXJfYnVpbHRpbnMzaW50M211bDhfX211bHRpMzE3aDcwZmZlZDI3MjQ1OWY5YjZFAF9aTjg0XyRMVCRpNjQkdTIwJGFzJHUyMCRjb21waWxlcl9idWlsdGlucy4ubWF0aC4ubGlibV9tYXRoLi5zdXBwb3J0Li5pbnRfdHJhaXRzLi5JbnQkR1QkMTJ3cmFwcGluZ19tdWwxN2hlY2EzZTNmZjVjYjI0YWYzRQBfWk42MF8kTFQkaTMyJHUyMCRhcyR1MjAkY29tcGlsZXJfYnVpbHRpbnMuLmludC4udHJhaXRzLi5ISW50JEdUJDE0emVyb193aWRlbl9tdWwxN2gxODA3NTFiZjAyMzdiZDMzRQBfWk40Y29yZTNudW0yMV8kTFQkaW1wbCR1MjAkaTY0JEdUJDEyd3JhcHBpbmdfbXVsMTdoMjcxMTM3ODZlYzY1YTU2MkUAbXVsPGkxMjg+AGZyb21fbG9faGk8aTEyOD4AL3J1c3RjL2U0MDg5NDdiZmQyMDBhZjQyZGIzMjJkYWYwZmFkZmU3ZTI2ZDNiZDEvbGlicmFyeS9jb21waWxlci1idWlsdGlucy9jb21waWxlci1idWlsdGlucy9zcmMvbGliLnJzL0AvY29tcGlsZXJfYnVpbHRpbnMuYzc5ZDYwYmVhOGJkMzg5NS1jZ3UuMDE5AC9ydXN0Yy9lNDA4OTQ3YmZkMjAwYWY0MmRiMzIyZGFmMGZhZGZlN2UyNmQzYmQxL2xpYnJhcnkvY29tcGlsZXItYnVpbHRpbnMvY29tcGlsZXItYnVpbHRpbnMvc3JjL2xpYi5ycy9AL2NvbXBpbGVyX2J1aWx0aW5zLmM3OWQ2MGJlYThiZDM4OTUtY2d1LjE3NgBfX211bHRpMwAvcnVzdGMvZTQwODk0N2JmZDIwMGFmNDJkYjMyMmRhZjBmYWRmZTdlMjZkM2JkMS9saWJyYXJ5L2NvbXBpbGVyLWJ1aWx0aW5zL2NvbXBpbGVyLWJ1aWx0aW5zL3NyYy9saWIucnMvQC9jb21waWxlcl9idWlsdGlucy5jNzlkNjBiZWE4YmQzODk1LWNndS4wNzMAL3J1c3RjL2U0MDg5NDdiZmQyMDBhZjQyZGIzMjJkYWYwZmFkZmU3ZTI2ZDNiZDEAL3J1c3RjL2U0MDg5NDdiZmQyMDBhZjQyZGIzMjJkYWYwZmFkZmU3ZTI2ZDNiZDEvbGlicmFyeS9jb3JlL3NyYy9saWIucnMvQC9jb3JlLjY2Y2I0NDU0MjA4ZTIwNTctY2d1LjAAY2xhbmcgTExWTSAocnVzdGMgdmVyc2lvbiAxLjk0LjEgKGU0MDg5NDdiZiAyMDI2LTAzLTI1KSkAAPQHCy5kZWJ1Z19saW5lywEAAAQARgEAAAEBAfsODQABAQEBAAAAAQAAAWxpYnJhcnkvY29tcGlsZXItYnVpbHRpbnMvY29tcGlsZXItYnVpbHRpbnMvc3JjAGxpYnJhcnkvY29tcGlsZXItYnVpbHRpbnMvY29tcGlsZXItYnVpbHRpbnMvc3JjL2ludABsaWJyYXJ5L2NvcmUvc3JjL251bQBsaWJyYXJ5L2NvcmUvc3JjL29wcwBsaWJyYXJ5L2NvbXBpbGVyLWJ1aWx0aW5zL2NvbXBpbGVyLWJ1aWx0aW5zL3NyYy9tYXRoLy4uLy4uLy4uL2xpYm0vc3JjL21hdGgvc3VwcG9ydAAAbWFjcm9zLnJzAAEAAHRyYWl0cy5ycwACAABpbnRfbWFjcm9zLnJzAAMAAGJpdC5ycwAEAABtdWwucnMAAgAAaW50X3RyYWl0cy5ycwAFAAAAAAUC/////wPdAwEEAgUVCgPrfMgGrAQDBQ0GA7QQIAQCBRUDu2+QBAMFDQPFECAEAgUVA7tvyAQDBQ0DxRAgA7h/PAQEBS0D5XFmBAMFDQObDiADyABYA7h/dAQEBS0D5XHkBAMFDQPjDoIGWAYDuH9YBAEFDgOsc1gCAQABAS0BAAAEACcBAAABAQH7Dg0AAQEBAQAAAAEAAAFsaWJyYXJ5L2NvbXBpbGVyLWJ1aWx0aW5zL2NvbXBpbGVyLWJ1aWx0aW5zL3NyYy9pbnQAbGlicmFyeS9jb21waWxlci1idWlsdGlucy9jb21waWxlci1idWlsdGlucy9zcmMAbGlicmFyeS9jb3JlL3NyYy9udW0AbGlicmFyeS9jb21waWxlci1idWlsdGlucy9jb21waWxlci1idWlsdGlucy9zcmMvbWF0aC8uLi8uLi8uLi9saWJtL3NyYy9tYXRoL3N1cHBvcnQAAHRyYWl0cy5ycwABAABtdWwucnMAAQAAbWFjcm9zLnJzAAIAAGludF9tYWNyb3MucnMAAwAAaW50X3RyYWl0cy5ycwAEAAAAegAAAAQAdAAAAAEBAfsODQABAQEBAAAAAQAAAWxpYnJhcnkvY29yZS9zcmMvb3BzAGxpYnJhcnkvY29tcGlsZXItYnVpbHRpbnMvY29tcGlsZXItYnVpbHRpbnMvc3JjL2ludAAAYml0LnJzAAEAAHRyYWl0cy5ycwACAAAAZgAAAAQANQAAAAEBAfsODQABAQEBAAAAAQAAAWxpYnJhcnkvY29yZS9zcmMAAHBhbmlja2luZy5ycwABAAAABQ4KAAUCWwAAAAPPAAEGA7B/SgICAAEBBREKAAUCAwAAAAOuAQECCAABAQCrAgRuYW1lAAcGcy53YXNtAYYCCQALa19zcGluX2xvY2sBFXpfdW5wZW5kX2ZpcnN0X3RocmVhZAIcYXJjaF90aHJlYWRfcmV0dXJuX3ZhbHVlX3NldAMOel9yZWFkeV90aHJlYWQEDHpfcmVzY2hlZHVsZQVJY29yZTo6cGFuaWNraW5nOjpwYW5pY19jb25zdDo6cGFuaWNfY29uc3RfYWRkX292ZXJmbG93OjpoYWNlYzk2NmRmMjMwYTc4ZgYWZ2FsZV9rX3NlbV9naXZlX2RlY2lkZQctY29yZTo6cGFuaWNraW5nOjpwYW5pY19mbXQ6Omg2NjUxMzEzYzNlMmM2YzJmCBF6X2ltcGxfa19zZW1fZ2l2ZQcSAQAPX19zdGFja19wb2ludGVyAJQBD3RhcmdldF9mZWF0dXJlcwgrC2J1bGstbWVtb3J5Kw9idWxrLW1lbW9yeS1vcHQrFmNhbGwtaW5kaXJlY3Qtb3ZlcmxvbmcrCm11bHRpdmFsdWUrD211dGFibGUtZ2xvYmFscysTbm9udHJhcHBpbmctZnB0b2ludCsPcmVmZXJlbmNlLXR5cGVzKwhzaWduLWV4dA==

On your CI heads-up — confirmed, and it's gale-wide. No gale Actions run has started since 13:08:34Z (~6h; now ~18:56) and there are no queued runs — so it's events-not-dispatching / runners-down, not just a backlog. Impact to flag: the nightly (my PR #61 board-target oracle), gale releases, and all PR CI are blocked until the runners are back. So the "build lands" timing for this depends on that recovering. Not your work to fix — flagging the dependency so we both know the release of the SROA fix waits on CI.

[avrabe]

3rd on-silicon data point + a scope note for the SROA design (G474RE, synth 0.11.45 / loom 1.1.14).

Stood up k_stack_push as the 3rd dissolved primitive. Struct-return family on real silicon now:

primitive	wasm-cross-LTO	native	ratio	decide ABI
k_sem_give	860 cyc	471	1.83×	u64-shaped (no sret)
k_mutex_unlock	472 cyc	124	3.81×	12-B struct (sret)
k_stack_push	252 cyc	56	4.5×	12-B struct (sret)

The scope note — the SROA plan we agreed on targets the u64 pack/unpack residue (the extend_i32_u/wrap_i64 ISLE terms), which is the sem shape. But the 51 struct-return decides (mutex/stack/msgq, ~majority of the surface) have a different residue that those terms won't touch: the inlined decide's 12-byte result struct is materialized in the wasm shadow frame and round-tripped through linear memory. Disasm of the dissolved z_impl_k_stack_push (synth 0.11.45):

; decide result written to the wasm shadow frame...
strb.w  r0, [fp, ip]      ; ip = frame+12  -> store `action` byte to linmem
...
ldrb.w  r0, [fp, ip]      ; read `action` back out of linmem
cmp ... beq/b              ; switch(d.action)

i.e. the struct never escapes (it's consumed by the very next switch in the same function after inline), yet it's spilled to the shadow stack and reloaded. That's a textbook SROA-through-inline case — but it's a struct scalarization + shadow-frame promotion, not a u64 wrap/extend. If the rewrite only adds the u64 ISLE terms, the struct-return family stays un-dissolved and keeps paying this round-trip (this is a big part of why stack is 4.5× — worst in the suite).

Recommendation (intent: please cover both in the SROA pass): when an inlined callee returns a struct by sret and the result doesn't escape the caller, scalarize the struct and keep its fields in SSA values / registers — eliminating the shadow-frame store+reload. Same proof-carrying discipline (Z3 obligation per rewrite) applies.

Kill-criteria (on-silicon gate = me):

• sem (as already agreed): no i64 pack/unpack in the dissolved body; re-measure 860→target.
• stack (new): no strb/ldrb of the decision struct through [fp, frame+N] in the dissolved body; re-measure 252→target. Repro harness: gale-smart-data/.../wasm-testbed/stack-microbench/ (one command, builds+flashes+measures both variants).

I'm staged to reflash + DWT-measure all three the moment a build lands.

[avrabe]

Absorbed the scope note — thanks for the 3rd data point. Confirming I'll cover both residue shapes under the same proof-carrying discipline, as two tracks:

1. u64 pack/unpack (sem shape) — the extend_i32_u/wrap_i64 ISLE terms + masked-forward rules. Landing the foundation now (the unconditional wrap_i64(extend_i32_u(x)) → x term-rewrite first, then the masked (...&mask→a; >>k→b) rules, each Z3-discharged).
2. struct-return via shadow-frame (mutex/stack/msgq — the majority, and the 4.5× worst case) — a different mechanism: linear-memory store→load forwarding for a non-escaping shadow-frame slot (prove the sret struct doesn't escape the caller post-inline, then scalarize its fields into SSA values and drop the strb/ldrb [fp,frame+N] round-trip). Same Z3 obligation per rewrite. This is the bigger structural win and I'll build it as track 2 once the u64 terms are in.

Kill-criteria noted for both (sem: no i64 pack/unpack; stack: no strb/ldrb of the decision struct through [fp,frame+N]). Will ping with a build for the 3-primitive reflash. Repro harnesses noted (stack-microbench/).

[avrabe]

Status + a key finding while building the SROA pass against your repro.

The u64 wrap/extend rewrite is in (live rewrite_pure_impl, Z3-validated per pass): wrap_i64(extend_i32_u(x)) → x, tested, suite green. But running it against sem.loom.wasm surfaced that the dissolution is blocked one step upstream — loom isn't inlining gale_k_sem_give_decide into z_impl_k_sem_give on this repro.

Evidence: loom optimize sem.loom.wasm --passes inline (and full default) leaves call $gale_k_sem_give_decide (decide-call count stays 1; pack/unpack op count 5→5). The pack lives in the decide (func 6: (extend_u(local0)<<32) | local3), the unpack in z_impl (func 8: t & 0xff, t >> 32) — two functions joined by the call. So the pack expression never reaches the unpack site, and no SROA rewrite (the wrap/extend identity or the planned masked &mask/>>k rules) can fire.

Root cause (confirmed in source): the inline gate function_inline_modelable is a strict instruction allowlist (arith / loads / stores / extend / wrap) that does not include Call, Block, Loop, If, Br, BrIf. gale_k_sem_give_decide has both — the nested-block dispatch and a call …panic_const_add_overflow (the semaphore-count overflow trap). So it's deemed non-modelable and stays an opaque call. The v1.1.6–v1.1.10 inline series handled the simpler straight-line decides; this one (control flow + a trap call) is beyond the current allowlist.

So the real next step for the sem shape is an inline-modelability extension — inline a decide that contains structured control flow and a divergent/trap call (panic-on-overflow never returns, so it's soundly modeled as "trap if reached"), with the Z3 by-body verifier extended accordingly. Then the existing dataflow local-forwarding brings the pack to the unpack and the SROA rules dissolve it.

Two checks for you: (1) does this match what you see — is the sem decide one that current loom leaves as a call (vs the mutex/stack shims it does inline)? (2) for the on-silicon 860→ target, the gating change is "inline the overflow-checked decide," and the SROA is the follow-on. I'll build the inline extension next (proof-carrying, same discipline) unless you'd rather I prioritize the struct-return shadow-frame track first.

[avrabe]

Q1: confirmed — and it's worse than "SROA can't fire": the sem seam is NOT dissolved at all, and my own gate was false-greening it. Thank you for surfacing this.

Measured on my artifacts (loom 1.1.14, --passes inline):

primitive	decide call post-loom	inlined?
k_sem_give	call $gale_k_sem_give_decide survives	✗
k_mutex_unlock	call $gale_k_mutex_unlock_decide survives	✗
k_stack_push	gone	✓ inlined

So your allowlist diagnosis is exactly right: stack_push's decide is straight-line (inlines); sem/mutex's decides have structured control flow + a panic_const_add_overflow trap call, so function_inline_modelable rejects them and they stay opaque calls.

The part I owe you a correction on: my "sem seam folded / 860 cyc" (and "mutex 472") were reported by a gate that greps the relocation for the public gale_k_*_decide symbol — but synth emits the surviving call against the renamed internal func_N symbol, so the grep found nothing and reported "folded." It's a false green. In the synth ARM output z_impl_k_sem_give really does bl <func_7> (= the decide; reloc R_ARM_THM_CALL func_7). I'm fixing the gate. So sem 860 / mutex 472 include the surviving decide call — the dissolution was never complete for these two.

Implication: your inline-modelability extension is a bigger win than "enables SROA." Dissolving the sem/mutex decide removes the decide bl + call/prologue overhead from 860/472 directly (a real cycle cut), and then the u64 wrap/extend SROA (already landed) + the masked rules dissolve the pack/unpack residue on top. Two wins stacked.

Q2 / prioritization — I'd do the inline-extension first. Reasoning: sem & mutex_unlock are the two highest-traffic primitives, both already on silicon (860/472), and both are u64-or-≤3-arg sret — no synth#359 dependency, so the inline-extension has a clean, immediately-measurable path to a silicon win. The struct-return shadow-frame track (mutex_lock/msgq/stack — the ≥4-arg sret family) is also gated on synth#359 (param0-as-sret recognition, still open), so it can't show a silicon delta until both loom-SROA and #359 land. Inline-extension = fastest demonstrable 860→ / 472→ improvement.

Kill-criteria (silicon, G474RE): after the inline-extension, (a) the dissolved z_impl_k_sem_give has no bl to the decide (I'll check the actual call target, not the renamed symbol this time), and (b) re-measure 860→. Repro unchanged (sem.loom.wasm). Ready to reflash on a build.

[avrabe]

Correction / scope-down on my last comment — I over-reached on one sentence; flagging it before it misleads.

What I've reliably verified holds:

• loom does not inline the sem (and mutex) decides — post---passes inline the call $gale_k_*_decide survives (count 5→5, the pack stays in the decide). Your allowlist diagnosis (control-flow + panic_const_add_overflow trap → function_inline_modelable rejects) is correct.
• My codegen "seam folded" gate was a false green: it grepped the relocation for the public gale_k_*_decide symbol, but synth renames the decide to an internal func_N and emits the call reloc against that — so the grep never saw it. For sem, the synth ARM provably still calls the decide (bl 130 <func_7>, func_7 == gale_k_sem_give_decide by nm alias). Gate fixed to disasm-based.

Where I over-reached: I said "sem 860 / mutex 472 include the surviving decide call." That conflates the loom level (decide not inlined — true for both) with the synth/ARM level (synth may still inline the call even when loom doesn't, and that's what actually runs). I have not rigorously established the per-primitive ARM-fold status — my quick bl-count is confounded by the mutex shim's helper funcs and is flag-dependent. So: sem is confirmed not-folded at ARM (decide bl survives); for mutex/pipe/fatal I'm re-measuring rigorously (per-function, resolving the decide's address) and will post the precise picture rather than an estimate. Sorry for the imprecise 472 claim.

Net for your work: the loom-side facts you need are unchanged — sem/mutex decides aren't loom-inlined, the inline-modelability extension (control-flow + trap-call) is the gating change, and it's higher-value than "enables SROA" because it also removes the decide call. I'll confirm the exact 860→ ARM delta on silicon once a build lands. Prioritization recommendation (inline-extension first, no synth#359 dependency) stands.

[avrabe]

The rigorous re-measurement I promised — complete loom-level dissolution map (reliable, wasm-tools-based, not the flaky objdump I walked back). "Dissolved" = call $gale_k_*_decide is gone after --passes inline:

primitive	decide call survives --passes inline?	dissolved?
k_sem_take	no	✅ dissolved
k_stack_push	no	✅ dissolved
k_stack_pop	no	✅ dissolved
k_sem_give	yes	❌
k_mutex_unlock	yes	❌
k_pipe_write	yes	❌
k_pipe_read	yes	❌
k_msgq_put	yes	❌

So the inline-modelability extension unblocks 5 of 8 measured primitives (sem_give, mutex_unlock, pipe_write, pipe_read, msgq_put), not just sem. The pattern matches your allowlist diagnosis exactly: the 3 dissolved decides are straight-line; the 5 un-dissolved ones have structured control flow and/or a trap call (panic_const_*) that function_inline_modelable rejects.

This both corrects my earlier "seam folded" claims (sem_give/pipe/mutex were never loom-dissolved — my reloc-name gate false-greened them) and quantifies the extension's leverage (5 primitives, incl. the two highest-traffic: sem_give 860, mutex_unlock 472). Per-ARM synth-fold of these survivors is a separate question I'm not asserting (needs a proper per-function tool, not greps — I'm not going to ship another flaky measurement). Prioritization stands: inline-extension first (sem_give/mutex_unlock have no synth#359 dependency → clean silicon win). Kill-criterion on a build: the dissolved body has no call $..._decide post-inline + re-measure 860/472→.