Module addr 

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

The validator itself lives in synth_core::static_data_addr — it must run on every compilation, and the shipping build is --features riscv, NOT verify, so a check gated on this (optional) crate would stay dormant in exactly the build that shipped #757 four times. It depends on nothing in synth-verify (no ordeal, no term), so it belongs in synth-core where the default compile path reaches it.

This module re-exports it so the VCR-VER-003 name resolves under synth-verify alongside the other translation-validation passes (it mirrors VCR-VER-002’s structure — a verdict enum + a per-compilation gate). See the synth-core module for the full invariant and the non-vacuous discrimination 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.

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).

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.

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).