feat(#777): VCR-VER-003 phase 2 — span validation + self-contained ROM-image gate + RV32 coverage

[avrabe]

VCR-VER-003 phase 2 (#777 follow-ups): span + self-contained + RV32 static-data validation

Phase 1 (v0.46) validated the single resolved addend byte per static-data reloc on the ARM32 relocatable mixed-split. This lands the three named follow-up classes, each red-first, with the validator staying unconditional (default --features riscv build).

1. Multi-byte access spans (mixed split) — VALIDATED, hard error

validate_reloc_resolutions_spanned: beyond the addend byte, every runtime-covered byte a conservatively-widened access (MAX_ACCESS_BYTES = 8; CodeRelocation records no width — the Abs32 literal is a pointer) could read must equal what the shipped packed init blob serves at that position. The .data emission now extends the validated blob, so the served side is the real artifact, not a recompute.

Red-first, demonstrated live: the staggered-overlap straddle fixture (seg_1 overwrites seg_0's tail; i32.load at 65542 spans into seg_1's runtime-owned bytes) compiled clean on the v0.46 binary — the packed seg_0 blob serves a4 a5 where the runtime image owns b0 b1, a silent miscompile no per-segment packing can serve. Phase 2 refuses it:

VCR-VER-003: static-data addressing validation FAILED — 4 relocation byte(s) disagree ...
  func 0 reloc @ 0xc (linmem 0x10006): __synth_wasm_seg_0+0x2 -> linmem 0x10008
  (span byte +2 of a possibly 8-byte access) serves 0xa4 but the runtime image owns 0xb0

Green companions: owner-resolved access on the same overlap compiles clean; gale's real mem757_gale/loom.wasm (same-start 3-overlap) stays green — same-start overlaps cannot produce a tail divergence under .rposition(), and the empirical anchor pins it. Documented residue: span bytes NO segment covers at runtime (implicit-zero linmem) are skipped — flagging them would hard-error the ubiquitous "pointer near a sparse segment's end, narrow access" shape; exact checking needs a recorded per-reloc access width (named follow-up).

Unit gates: phase1_green_but_span_red_on_staggered_overlap (the same input is phase-1-Consistent and phase-2-Mismatch — non-vacuity), span_red_on_padding_shifted_crossing (4-align pad breaks linmem adjacency), span_red_on_init_region_escape, span_green_on_adjacency_preserving_crossing, span_green_on_sparse_tail.

2. Self-contained --cortex-m ROM-copy (#758) — VALIDATED, hard error

The dense flash image is now packed by the shared declaration-order packer (pack_rom_image) and validated unconditionally against the independently reconstructed runtime image (validate_served_image: every blob byte equals the later-wins byte, zero in gaps). The dense layout (index = linmem offset) preserves spans/overlaps structurally — the straddle fixture the mixed split refuses compiles correctly here (e2e green gate asserts the #758 image is present and the validator silent).

Red-first: the overwrite policy is an argument (phase 1's resolve_owner pattern) — rom_image_red_on_first_wins_green_on_last_wins pins Mismatch on the first-wins pack (stale 0xAA at the classic #757 offset vs runtime 'u') and Consistent on declaration order; rom_image_gap_garbage_red_zero_tail_green pins gap-garbage red / zero-tail green.

3. RV32 static bases — VALIDATED (loud warning) + documented

RV32 is a single-base scheme (s11 = __linear_memory_base, zeroed RAM; no per-segment relocs, so the #757 wrong-segment class is unrepresentable). Probing found the real gap: the object is .text-only and active nonzero data segments are silently dropped (loads read 0x00). validate_served_image with an empty image now runs unconditionally on the RV32 emit path and warns loudly per un-served nonzero byte; all-zero / zero-overwritten runtime images genuinely ARE served by zeroed RAM and stay silent (a later-wins check, not a bytes grep — rv32_zero_overwritten_data_stays_silent).

Held at warning, not a hard decline: the CI-pinned RV32 frozen fixture (control_step.wasm carries a nonzero segment its differential never reads) freezes compile-success on this path. Hard decline + initializer shipping (the RV32 analogue of #758: linker-script placement + startup copy) is the named follow-up.

4. AArch64 — documented N/A (verified, not fabricated)

The -b aarch64 integer subset has no linear-memory loads/stores (every memory op loud-declines at selection: unsupported wasm op for aarch64 subset: I32Load), so compiled code cannot observe static data — nothing to validate.

Gates

• cargo test --workspace green (125 suites, 0 failures); cargo fmt --check + cargo clippy --workspace --all-targets -- -D warnings clean
• All static-data differentials pass against this branch: mem757_gale, self_contained_data_758, multi_segment_static_data, static_above_sp_739, wide_static_746, wide_static_copy_757, mem757_rawvec_memcopy, multi_memory_406
• All 13 RV32 differentials pass (incl. control_step — the new warning is byte-invisible to .text); RV32/ARM frozen fixtures bit-identical
• python3 scripts/claim_check.py claims.yaml → 21/21 (new count-eq pins hold the phase-2 wiring unconditional); rivet check clean
• Docs + ledger bumped together: roadmap VCR-VER-003 phase-2 items (5)–(8), claims.yaml, CLAUDE.md Track C

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[avrabe]

RV32 initializer-shipping + hard-decline follow-up filed as #798 (the named follow-up held at warning in this PR).

[codecov]

Codecov Report

❌ Patch coverage is 94.57143% with 19 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-core/src/static_data_addr.rs	95.72%	13 Missing ⚠️
crates/synth-cli/src/main.rs	86.95%	6 Missing ⚠️

📢 Thoughts on this report? Let us know!