Module static_data_addr 

Static-data addressing validation (VCR-VER-003, synth #777 / #757).

WASM active data segments are applied to linear memory in declaration order, later-wins: when two active segments overlap the same range, the later-declared one overwrites the earlier. synth’s --native-pointer-abi relocatable path splits the linear memory into one packed .data blob per segment (__synth_wasm_seg_K) and retargets every static-data relocation __synth_wasm_data + C to __synth_wasm_seg_K + (C - seg_off_K) (the #354 mixed-split). Choosing the WRONG owning segment for an address C that lies in several overlapping segments is a silent miscompile: the reloc reads a stale earlier segment’s bytes instead of the byte the runtime image holds.

This is exactly #757 — gale’s fused gust:os node declared three active segments all at linmem 0x100000; the string lived in the last segment but the retargeting (.position()) bound its reads to the first segment’s consts (got=[2,0,0,0,..] = __synth_wasm_seg_0+8). It survived four releases because value-differential oracles are coverage-limited (7 synthetic reconstructions were all green). The fix resolves overlapping addresses to the LAST-declared owner (.rposition()).

What this validator proves (per compilation, by construction)

Given the module’s active data segments (declaration order) and the retargeting the compiler actually emitted — one RelocResolution (seg_index K, addend A) per static-data reloc — it reconstructs the RUNTIME linear-memory image (apply every segment in declaration order, later-wins) independently of K, then asserts: the byte the packed .data serves for that reloc (seg[K].bytes[A]) EQUALS the byte the runtime image holds at the reloc’s original access address (seg[K].off + A). A single mismatch — the wrong-segment resolution — is a Verdict::Mismatch.

Concrete, not symbolic; unconditional

This is a concrete byte-equality over a compiled object, not a ∀-inputs SMT property, and it depends on nothing but std — so it lives in synth-core and runs on every compilation (the shipping build is --features riscv, not verify; a verify-gated check would stay dormant in exactly the build that shipped #757 four times). It mirrors VCR-VER-002’s structure (a verdict enum + a per-compilation gate) but does the honest thing — a direct comparison against an independently reconstructed truth image. The truth side never touches K, so the validator cannot be satisfied by mirroring the code under test (the mirror-pinning vacuity mode is structurally excluded). synth-verify re-exports this module for the VCR-VER-003 tests.

Phase 2 (#777 follow-ups)

Phase 1 validated the single resolved addend byte per reloc. Phase 2 extends coverage to the named follow-up classes:

1. Multi-byte access spans (validate_reloc_resolutions_spanned): a reloc whose addend byte is runtime-correct can still mis-serve TAIL bytes — an i32/i64 load starting in segment K whose span crosses into a range a LATER-declared segment owns at runtime (staggered overlap), or crosses K’s packed end into 4-align padding / the next declared (not next linmem) segment. The access width is not recorded on crate::backend::CodeRelocation (the Abs32 literal is a pointer; its consumers are ldrb/ldrh/ldr/ldrd), so the span is validated conservatively out to MAX_ACCESS_BYTES with one deliberate tolerance: a span byte whose runtime address NO segment covers is skipped (implicit-zero linear memory — flagging it would hard-error the ubiquitous “pointer near the end of a sparse segment, narrow access” shape). A span byte that IS runtime-covered must match what the packed blob actually serves at that position, byte-for-byte, so the served side reads the EMITTED init blob (PackedInit) — never a recompute.
2. Dense served images (validate_served_image / pack_rom_image): the self-contained --cortex-m ROM-copy layout (#758) serves linear memory from ONE dense flash blob copied to RAM at reset — index = linmem offset, so spans/overlaps are structurally preserved and the whole obligation reduces to “every blob byte equals the runtime image byte (later-wins, zero elsewhere)”. The RISC-V single-base scheme (#798) ships its active segments as SPARSE per-segment records (pack_segment_records, a .wasm_data PROGBITS section in flash) which the generated startup copies to s11 + off in record order at reset; the emit path READS BACK the emitted blob (served_image_from_records — never a recompute, that would mirror-pin the check) into the dense served image and runs the same gate, hard-erroring the compile on any served/runtime disagreement. An EMPTY image models a target that ships no initializer bytes at all (zeroed RAM serves every address): any nonzero runtime-image byte is then a served/runtime mismatch (the silent initializer-drop this validator caught on the pre-#798 RV32 path).
3. AArch64: N/A — the -b aarch64 integer subset has no linear-memory loads/stores (every memory op loud-declines at selection), so compiled code cannot observe static data; there is nothing to validate.

Structs

AddrMismatch

A single reloc that reads the wrong byte.

DataSegment

One active WASM data segment: its linear-memory offset and its bytes, in declaration order. The packed .data blob stores these bytes verbatim (4-aligned per segment) under __synth_wasm_seg_K; index K in the segment list is the K in the symbol name.

ImageMismatch

One dense-image byte that disagrees with the runtime image.

PackedInit

The EMITTED packed-.data init region of the #354 mixed split: each segment’s bytes at its 4-aligned packed offset, in declaration order, EXCLUDING the trailing __synth_globals slots. Both fields are read back from what the compiler actually laid out / filled — the validator never recomputes the packing (that would mirror-pin the check).

RelocResolution

The retargeting the compiler emitted for one static-data relocation: it now points at __synth_wasm_seg_{seg_index} + addend. seg_index is the K from the emitted symbol name; addend is the emitted in-place REL addend (= original_access_addr - seg[K].linmem_off). This is the value read back from what the compiler produced — NEVER recomputed by the validator (that would mirror-pin the check and make it vacuous).

Enums

ImageVerdict

The verdict of a dense served-image gate (validate_served_image).

Verdict

The verdict of the addressing gate.

Constants

MAX_ACCESS_BYTES

The widest scalar linear-memory access synth can emit (i64.load / i64.store — there is no v128 support on these paths). Conservative span bound used when a reloc’s true access width is unknown.

Functions

image_extent

Total extent of the runtime image: max(off + len) over the segments (u64, so a hostile off + len cannot wrap — callers bound-check against the linear-memory size before packing).

pack_rom_image

Pack the #758 dense ROM init image: a [0, extent) blob with every active segment placed AT its linmem offset. last_wins = true applies them in declaration order (WASM instantiation semantics — later segments overwrite earlier on overlap); last_wins = false applies them in REVERSE order (first-wins — the synthetic miscompile the red-first gate toggles, phase 1’s resolve_owner pattern). The caller must have bound-checked image_extent against the linear-memory size (u32 + usize safe here only after that check).

pack_segment_records

Pack active data segments into the sparse per-segment record blob the RV32 backend ships as its .wasm_data PROGBITS section (#798). Format, repeated per segment in DECLARATION order:

parse_segment_records

Parse a .wasm_data record blob back into (linmem_off, bytes) records, in record order. Returns None on a malformed blob (truncated header or payload, misaligned trailing bytes) — the read-back side of the #798 served-image gate must fail LOUDLY on garbage, never “best-effort” it.

resolve_owner

Resolve an access address c to its owning segment index under a chosen tie-break policy, mirroring main.rs’s .rposition() / .position() search. last_wins = true is the CORRECT WASM overwrite semantics (.rposition()); last_wins = false is the #757 miscompile (.position()). Returns the segment index and the addend c - seg.linmem_off, or None if c is in no segment. Exposed so the red-first gate can toggle the policy as an argument (no source revert), and so callers can build resolutions the same way the compiler does.

served_image_from_records

Reconstruct the dense image the shipped records SERVE: apply every record to __linear_memory_base-relative addresses in RECORD order (later overwrites earlier), exactly what the generated startup’s copy loop does at reset. This is the read-back side of the #798 gate — it consumes the EMITTED blob, so feeding it to validate_served_image against the declared segment list cannot be satisfied by mirroring the packer. Returns None on a malformed blob, or when a record’s off + len overflows u32 (a hostile extent that could never be served).

validate_reloc_resolutions

The per-compilation addressing gate. For every emitted RelocResolution, assert the packed byte it serves equals the runtime-image byte at the original access address. See the module docs for the invariant.

validate_reloc_resolutions_spanned

Phase-2 (#777) per-compilation addressing gate: the phase-1 addend-byte check PLUS a conservative multi-byte span check per reloc.

validate_served_image

Dense served-image gate: for every address in [0, image_extent), the byte SERVED — image[addr], or 0 when the image doesn’t reach addr (zeroed RAM; an empty image models a target that ships NO initializer bytes, the RISC-V single-base scheme) — must equal the runtime image byte (segments applied in declaration order, later-wins; implicit zero where uncovered).