Summary
The #791 fix made _ShadowGuard.push (vera/runtime/heap.py) bound the full 4-byte slot (sp < 0 or sp + 4 > limit). The sibling sweep in that PR found four structurally-identical sp >= limit-then-write-4-bytes bounds elsewhere, each protected by the same invariant (generated code always advances gc_sp in 4-byte aligned steps):
- vera/wasm/helpers.py:135-140 — the
gc_shadow_push WAT emitter (i32.ge_u → unreachable before a 4-byte store)
- vera/codegen/assembly.py:883-887 — the
$register_wrapper slow-path root push (same WAT shape)
- vera/browser/runtime.mjs:127 —
gcRooted
- vera/browser/runtime.mjs:1555 —
gcShadowPush
Why a follow-up, not part of the burndown
Classified as hardening (enhancement), not bug, per the same reasoning as #791's honest framing: the misaligned state is unreachable while the alignment invariant holds, and no documented promise is violated. Unlike #791's one-liner, the WAT-emitter changes churn every emitted module (golden-WAT pins re-baseline), so the cost profile is different. If the maintainer prefers to treat this class as bugs (matching #791's original label), relabel and it joins the v0.1.0 gate.
Fix sketch
Same slot-complete form in all four sites; the two WAT sites need the emitted guard updated plus a golden-pin re-baseline; the two runtime.mjs sites are one-liners plus a browser-side unit test mirroring TestShadowGuardPushBound791.
Summary
The #791 fix made
_ShadowGuard.push(vera/runtime/heap.py) bound the full 4-byte slot (sp < 0 or sp + 4 > limit). The sibling sweep in that PR found four structurally-identicalsp >= limit-then-write-4-bytes bounds elsewhere, each protected by the same invariant (generated code always advancesgc_spin 4-byte aligned steps):gc_shadow_pushWAT emitter (i32.ge_u→unreachablebefore a 4-byte store)$register_wrapperslow-path root push (same WAT shape)gcRootedgcShadowPushWhy a follow-up, not part of the burndown
Classified as hardening (enhancement), not bug, per the same reasoning as #791's honest framing: the misaligned state is unreachable while the alignment invariant holds, and no documented promise is violated. Unlike #791's one-liner, the WAT-emitter changes churn every emitted module (golden-WAT pins re-baseline), so the cost profile is different. If the maintainer prefers to treat this class as bugs (matching #791's original label), relabel and it joins the v0.1.0 gate.
Fix sketch
Same slot-complete form in all four sites; the two WAT sites need the emitted guard updated plus a golden-pin re-baseline; the two runtime.mjs sites are one-liners plus a browser-side unit test mirroring
TestShadowGuardPushBound791.