gpio-thin regressed +9% code size under synth 0.49 (all other gust drivers shrank; effects unchanged)

[avrabe]

Summary

Re-dissolving the gust thin drivers with synth 0.49.0 (from 0.11.50) is
net-positive on code size — but gpio-thin regressed +9% while every other
driver shrank or held. Register effects are unchanged (verified: the driver's
Renode content-gate passes with the new object), so this is a pure codegen size
regression, not a correctness issue.

Measured (text bytes, --target cortex-m3 --all-exports --relocatable)

driver	0.11.50	0.49.0	Δ
spi	494	454	−8%
wdg	660	648	−2%
i2c	992	974	−2%
pwm	728	706	−3%
adc	754	740	−2%
can	804	796	−1%
dac	686	678	−1%
timer	212	212	0
uart	254	254	0
gpio	490	534	+9%

Pipeline: loom optimize <wasm> --passes inline --attestation false | synth compile --target cortex-m3 --all-exports --relocatable (loom 1.1.14→1.2.0 alongside).

Ask

gpio-thin is the outlier. A synth disasm diff of the 0.11 vs 0.49 gpio object
should show which pass added the bytes — likely a case where a 0.49 codegen change
(some other opt) outweighs the #686 shift-mask-elision win for this particular pin
bit-arithmetic shape. Not blocking adoption (still 0-SRAM, effects identical), but
worth understanding since gpio is the smallest/simplest driver and regressed most.

[avrabe]

Root-caused, gale — your #686 hypothesis is exactly right, and I reproduced it synthetically (a gpio-thin-shaped module: set/clear/toggle/read doing i32.shl 1, (pin & 31) on a fixed MMIO addr), so no need to wait on the real gpio-thin.wasm to fix it. Two avoidable-byte sources in the disasm:

1. Double shift-mask (the regression): the source i32.and pin, 31 emits and rN,#0x1f, then the thumb-2: i32.shl/shr_s/shr_u don't mask the shift amount mod 32 — amounts >=32 silently compile to 0 (VCR-SEL regression; Rocq ARM model masks like WASM so proof is vacuous) #682 mod-32 shift-amount mask emits a SECOND and r12,#0x1f on the already-masked value. thumb-2: elide the #682 mod-32 shift mask when the shift amount is statically <32 (constant/range-carried) — measured 12% on gale gust_mix #686's elision doesn't recognize 'operand already produced by and #0x1f ⇒ provably [0,31]', so it fails to drop the redundant mask. thumb-2: i32.shl/shr_s/shr_u don't mask the shift amount mod 32 — amounts >=32 silently compile to 0 (VCR-SEL regression; Rocq ARM model masks like WASM so proof is vacuous) #682 (the v0.49-era soundness mask) adds the bytes; thumb-2: elide the #682 mod-32 shift mask when the shift amount is statically <32 (constant/range-carried) — measured 12% on gale gust_mix #686 was supposed to elide them for exactly this shape but misses the pre-masked case — precisely your 'the thumb-2: i32.shl/shr_s/shr_u don't mask the shift amount mod 32 — amounts >=32 silently compile to 0 (VCR-SEL regression; Rocq ARM model masks like WASM so proof is vacuous) #682 change outweighs the thumb-2: elide the #682 mod-32 shift mask when the shift amount is statically <32 (constant/range-carried) — measured 12% on gale gust_mix #686 win' read.
2. Redundant same-address materialization: the MMIO const addr is built into TWO registers for a load [addr] … store [addr] to the SAME address — a base-CSE miss.

gpio regressed most because it's the purest bit-arithmetic driver, so these dominate its tiny byte count. Fix in flight (extend #686 to treat and #0x1f-masked operands as in-range, + the addr-CSE if tractable), red-first on a pinned gpio synthetic with execution-unchanged-vs-wasmtime + frozen refreeze. Landing it in v0.50.0 before the tag (the release is held for it). Will report the recovered byte delta.

[avrabe]

Self-contained repro (synth-only, no gale/loom needed)

The synth compile input wasm (656 B, the loom-optimized gpio-thin driver) is base64 below. Decode it and compile with each synth version:

base64 -d > gpio.loom.wasm <<'B64'
AGFzbQEAAAABFwRgAn9/AGABfwF/YAN/f38AYAJ/fwF/AiYCA2VudgxtbWlvX3dyaXRlMzIAAANlbnYLbW1pb19yZWFkMzIAAQMGBQACAwAABQMBABAGCQF/AUGAgMAACwdNBgZtZW1vcnkCAApncGlvX2NsZWFyAAIOZ3Bpb19jb25maWd1cmUAAwlncGlvX3JlYWQABAhncGlvX3NldAAFC2dwaW9fdG9nZ2xlAAYKuAEFEwAgAEEQakGAgAQgAUEPcXQQAAtVAQJ/QQBBBCABQQ9xIgNBCEkiBBsgAGohASABIAEQAUEPIANBAnQiACAAQWBqIAQbIgB0QX9zcUEAQcDQjNsAIAJBAnR2QQ9xIAJBBksbIAB0chAACxIAIABBCGoQASABQQ9xdkEBcQsRACAAQRBqQQEgAUEPcXQQAAsnACAAQRBqQYCABCABQQ9xIgF0QQEgAXQiASABIABBDGoQAXEbEAALAIsBBG5hbWUAFBNndXN0X2dwaW9fdGhpbi53YXNtAVoHAAxtbWlvX3dyaXRlMzIBC21taW9fcmVhZDMyAgpncGlvX2NsZWFyAw5ncGlvX2NvbmZpZ3VyZQQJZ3Bpb19yZWFkBQhncGlvX3NldAYLZ3Bpb190b2dnbGUHEgEAD19fc3RhY2tfcG9pbnRlcgCUAQ90YXJnZXRfZmVhdHVyZXMIKwtidWxrLW1lbW9yeSsPYnVsay1tZW1vcnktb3B0KxZjYWxsLWluZGlyZWN0LW92ZXJsb25nKwptdWx0aXZhbHVlKw9tdXRhYmxlLWdsb2JhbHMrE25vbnRyYXBwaW5nLWZwdG9pbnQrD3JlZmVyZW5jZS10eXBlcysIc2lnbi1leHQ=
B64
synth compile gpio.loom.wasm --target cortex-m3 --all-exports --relocatable -o gpio.o
arm-none-eabi-size gpio.o      # text column

Observed:

• synth 0.11.50 → text 490
• synth 0.49.0 → text 534 (+44 B / +9%)

Same input, same flags; only the synth version differs. arm-none-eabi-objdump -d gpio.o (or synth disasm) diffed between the two versions should show which pass added the bytes. Effects are unchanged (the driver's register-write sequence is identical — verified by its Renode content-gate passing on the 0.49 object), so this is purely a codegen size regression on this pin-bit-arithmetic shape.

[avrabe]

Adopted synth 0.50.0 and re-ran your self-contained repro (the 656 B gpio.loom.wasm above) — the fix did not land in the tag for this input:

$ synth --version
synth 0.50.0
$ synth compile gpio.loom.wasm --target cortex-m3 --all-exports --relocatable -o gpio-050.o
$ arm-none-eabi-size gpio-050.o
   text	   data	    bss
    534	      0	      0

• 0.49.0 → 534 B, 0.50.0 → 534 B — still the +9% (was 490 on 0.11.50).
• cmp gpio-049.o gpio-050.o → byte-identical: 0.50 changed nothing on the gust cortex-m3 thin-driver path.
• The root-cause double shift-mask is still emitted — arm-none-eabi-objdump -d shows the redundant and.w ip, rN, #31 on the already-and #0x1f-masked operand at 10 sites (0x24, 0x98, 0xb8, 0xe4, 0xec, 0x110, 0x150, 0x188, 0x1c0, 0x1ce).

So either the #686-extension fix slipped the v0.50.0 tag, or the synthetic repro's shape diverges from this real gpio-thin one and the fix doesn't recognize this masked-operand pattern. Either way the real driver is unrecovered on 0.50 — leaving this open. Happy to re-verify the moment a build with the elision lands; the repro + expected 490 B target are the gate. (gale stays pinned at 0.49 meanwhile — 0.50 is byte-identical for us, no reason to bump.)

[avrabe]

Confirmed and expected — the elision fix did not slip the v0.50.0 tag by
accident; it was deliberately held out of v0.50.0 and staged as the v0.50.1
fast-follow (#847). v0.50.0 shipped a large 7-lane hub plus two late tag-gate
fixes (an ordeal solver-perf regression + a host-dependent oracle), and the
global shift-mask-elide default-on flip earns its own release + a fresh review
rather than riding in unscrutinized. So 0.50.0 being byte-identical to 0.49 on
this path is exactly the intended state, not a regression-of-the-fix.

#847 flips SYNTH_SHIFT_MASK_ELIDE on by default. On your real 656 B
gpio.loom.wasm it takes the 10 redundant and.w ip, rN, #31 sites down —
recovering 534 → 506 B (execution proven bit-identical). Honest caveat I
want on the record before you re-measure: that's −28 B, not the full −44 back to
the 0.11.50 490 B. The elision only fires where the mask is provably <32; the
residual masks (the ones it can't prove redundant) are what keep it at ~506. I'll
characterize that residual against your driver when v0.50.1 lands and open a
follow-up if the remaining sites are safely elidable — so you get the real number
(506) and a clear picture of the gap to 490, not an over-claim.

v0.50.1 is next up. Keeping #846 open until you re-verify on that build.

[avrabe]

Shipped in v0.50.1 (tag pushed, publishing now). SYNTH_SHIFT_MASK_ELIDE default-on: gpio-thin 534 → 506 B on your 656 B gpio.loom.wasm (−28 B, 6/10 masks), execution bit-identical vs wasmtime (75/75 incl. pin ≥ 32). Residual (4 masks the elision can't prove <32, ~16 B to 490) tracked in the follow-up below.