track(#354): GI-NPA-004 + repro — per-region .bss/.data split for high-offset init segments (#355)

gale #354: the #345 zero-init split is binary (split_linmem_bss = native_layout
&& data_segments.is_empty()), so ANY initialized (data) segment makes the whole
[0, used_extent) linmem image PROGBITS. A dissolved stack_push seam carries a
12-byte .rodata const (-12/-ENOMEM) at linmem offset 65536, above the 64 KiB
shadow stack → 65552-byte PROGBITS .data (MCU-unshippable; mutex is .data=4).

This is the mixed-case deferred in the #345 code comment coming due — NOT a
v0.11.44 regression; #350 just made stack_push compile far enough to expose it.

- artifacts/gale-integration.yaml: GI-NPA-004 (sw-req, proposed, release-v0.11.45).
  Design: per-region SYMBOLS (zero reservation keeps __synth_wasm_data/.bss; each
  init segment gets its own PROGBITS section + symbol; selector relocates each
  static access against its region's symbol) — link-survivable, unlike a naive
  per-section split (single base symbol + baked addends need contiguity the
  linker won't grant). Sound iff init-data is statically separable from the zero
  region — to confirm against gale's stack_push.loom.wasm before implementing.
- scripts/repro/high_offset_init_segment_354.wat: minimal reconstruction (SP
  global init 65536 + 12-byte init segment at 65536 + static load at addr 65544)
  that reproduces .data=65552 locally with --native-pointer-abi --relocatable.

Implementation (selector + ELF) is the next feature-loop; this commit tracks +
secures the repro. Frozen differentials unaffected (no code change here).

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: avrabe

artifacts/gale-integration.yaml

@@ -516,3 +516,51 @@ artifacts:
       pass-criteria: >
         Linked dissolved seam runs with no runtime and matches the native
         reference behavior; no MPU fault from mis-addressed statics or stack.
+
+  - id: GI-NPA-004
+    type: sw-req
+    title: Per-region .bss/.data split for high-offset init segments (#354)
+    description: >
+      The #345 zero-init split is binary: `split_linmem_bss =
+      native_layout.is_some() && data_segments.is_empty()` (synth-cli
+      build_relocatable_elf). When ANY initialized `(data)` segment is
+      present the whole `[0, used_extent)` linmem image is emitted as one
+      PROGBITS `.data`. gale #354: a dissolved stack_push seam carries a
+      12-byte `.rodata` const (`0xfffffff4` = -12/-ENOMEM) at linmem offset
+      65536 — above the 64 KiB shadow stack — so the entire zero stack-gap
+      ships as 65552 bytes of PROGBITS `.data` (MCU-unshippable; the mutex
+      seam, with no init segment, is `.data=4`/`.bss=65536`). synth shall
+      split the linmem image PER REGION: each initialized byte-range as a
+      small PROGBITS section and the surrounding zero runs as SHT_NOBITS
+      `.bss`, so `.data` is bounded to the initialized bytes. Because a
+      single `__synth_wasm_data` base symbol + selector-baked addends cannot
+      span independently-placed sections (the link-fragility deferred in the
+      #345 code comment), the split shall use PER-REGION SYMBOLS: the zero
+      reservation keeps `__synth_wasm_data` (.bss); each init segment gets
+      its own PROGBITS section + symbol; the selector relocates each static
+      access against the symbol of the region the offset falls in. Sound
+      only if init-data accesses are statically separable from the zero
+      region (the rodata const is reached only by a static address, never by
+      a dynamic pointer that also walks the shadow stack) — to be confirmed
+      against gale's stack_push.loom.wasm before implementation.
+    status: proposed
+    tags: [gale, native-pointer-abi, bss, elf, mcu-shippability, release-v0.11.45]
+    links:
+      - type: derives-from
+        target: GI-NPA-001
+      - type: traces-to
+        target: gale:354
+    fields:
+      req-type: functional
+      priority: must
+      verification-criteria: >
+        scripts/repro/high_offset_init_segment_354.wat (SP global init
+        65536 + 12-byte init segment at 65536 + a static load at addr
+        65544) compiled with --native-pointer-abi --relocatable
+        --all-exports yields `.data` bounded to the initialized bytes (~12 B)
+        with the zero stack-gap as SHT_NOBITS `.bss` (matching the mutex
+        shape); mutex_unlock stays `.data=4`/`.bss=65536`; the four frozen
+        differentials (control_step 0x00210A55, flight_seam 0x07FDF307,
+        div_const 338/338, mutex_pressure) stay byte-identical; gale's
+        stack_push runs correctly on G474RE (loads the -12 const, walks the
+        shadow stack) under the differential oracle.

scripts/repro/high_offset_init_segment_354.wat

@@ -0,0 +1,8 @@
+(module
+  (memory (export "memory") 2)
+  (global $sp (mut i32) (i32.const 65536))
+  (data (i32.const 65536) "\00\00\00\00\00\00\00\00\f4\ff\ff\ff")
+  (func (export "stack_push_decide") (result i32)
+    ;; static address >= wasm_data_base (65536) -> __synth_wasm_data-relative
+    i32.const 65544
+    i32.load))