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.

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.