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.

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.

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

Verdict

The verdict of the addressing gate.

Functions

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.

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.