synth_verify/addr.rs
1//! Static-data addressing validation (VCR-VER-003, synth #777 / #757).
2//!
3//! The validator itself lives in [`synth_core::static_data_addr`] — it must run
4//! on **every** compilation, and the shipping build is `--features riscv`, NOT
5//! `verify`, so a check gated on this (optional) crate would stay dormant in
6//! exactly the build that shipped #757 four times. It depends on nothing in
7//! `synth-verify` (no ordeal, no `term`), so it belongs in `synth-core` where
8//! the default compile path reaches it.
9//!
10//! This module re-exports it so the VCR-VER-003 name resolves under
11//! `synth-verify` alongside the other translation-validation passes (it mirrors
12//! VCR-VER-002's structure — a verdict enum + a per-compilation gate). See the
13//! `synth-core` module for the full invariant and the non-vacuous discrimination
14//! tests.
15
16pub use synth_core::static_data_addr::{
17 AddrMismatch, DataSegment, ImageMismatch, ImageVerdict, MAX_ACCESS_BYTES, PackedInit,
18 RelocResolution, Verdict, image_extent, pack_rom_image, resolve_owner,
19 validate_reloc_resolutions, validate_reloc_resolutions_spanned, validate_served_image,
20};