feat(#777): VCR-VER-003 — per-compilation static-data addressing validation (the #757 miscompile class made unrepresentable)

[avrabe]

VCR-VER-003 (#777, epic #242) — Wave-1 Lane 1

Lifts the post-hoc #757 differential oracle (scripts/repro/mem757_gale_differential.py) into a per-compilation validator, so the overlapping-active-segment wrong-segment miscompile FAILS at compile time on any module instead of shipping silently. #757 survived four releases because value-differential oracles are coverage-limited (7 synthetic reconstructions were all green; only gale's real fused gust:os node hit it).

The invariant (concrete byte-equality, not SMT)

For a compiled relocatable object with N active data segments, for every emitted static-data relocation (symbol = __synth_wasm_seg_K, addend A): the byte the packed .data serves (seg[K].bytes[A]) EQUALS the byte the runtime linear-memory image holds at the original access address (seg[K].off + A), where the runtime image applies every active segment in WASM declaration order, later-wins.

The runtime image is reconstructed independently of the chosen K — it is derived only from the segment list — so the truth side never mirrors the code under test. The mirror-pinning vacuity failure mode is structurally excluded.

There are no symbolic operands (unlike VCR-VER-002's trap VCs), so this is an honest direct byte-comparison, not fabricated SMT. Claim wording matches.

Unconditional (runs in the shipping build)

The validator lives in synth_core::static_data_addr and is called directly in the mixed-split reloc retargeting path (synth-cli/src/main.rs). It runs on every compilation — the shipping/release build is --features riscv, not verify (confirmed release.yml L33-39), so a verify-gated check would have stayed dormant in exactly the build that shipped #757 four times. synth-verify::addr re-exports it (VCR-VER-002 structure parity), single source, no mirror drift.

Trigger scope: the check fires on the native-pointer relocatable mixed-split path (--native-pointer-abi --relocatable + the mixed_separable geometry) — the only path that emits per-segment __synth_wasm_seg_K retargets, and thus the only path the #757 class can arise on. On a Mismatch the compile hard-errors (anyhow::bail!) naming the offending symbol/addend/served/runtime bytes.

Non-vacuous, red-first gate

Permanent discrimination unit test (synth_core::static_data_addr::red_on_first_match_green_on_last_match): the SAME validator, on a synthetic 3-overlap module with distinct bytes, returns Mismatch on the .position() (first-match, the #757 bug) resolution and Consistent on the .rposition() (last-match, correct) resolution. The tie-break is an argument (resolve_owner(last_wins)), so this is a permanent test, not a one-time source revert. Plus partial-overlap-tail-wins, non-overlapping-both-consistent, out-of-range-mismatch.

Durable end-to-end gate (synth-cli/tests/vcr_ver_003_addr_777.rs): compiles gale's real loom.wasm and asserts exit 0. Because the validator is wired unconditionally, this GREEN goes RED the instant main.rs reverts .rposition() → .position(). Empirically confirmed both directions:

# .rposition() (shipped):  test gale_overlapping_segments_compile_clean ... ok
# .position()  (reverted): test gale_overlapping_segments_compile_clean ... FAILED
#   Error: VCR-VER-003: static-data addressing validation FAILED — 1 relocation(s)...
#     func 9 reloc @ 0x250: __synth_wasm_seg_0+0x8 -> linmem 0x100008
#       serves 0x02 but the runtime image owns 0x67

0x02 is exactly gale's historical got=[2,0,0,0,..] = __synth_wasm_seg_0+8; 0x67 = 'g', the string's real first byte. The gale GREEN is non-vacuous — the RED demo proved gale actually reaches the retarget path (func 9 reloc @ 0x250 fired), so GREEN means "validator ran and passed," not "never executed." (Honours the "the real module must live in CI; synthetic shapes were all green" lesson.)

Ledger / status

• claims.yaml: new SYNTH-VCR-VER-003-STATUS (20/20 claims hold).
• artifacts/verified-codegen-roadmap.yaml: VCR-VER-003 added, status implemented.
• CLAUDE.md: Track C North Star note.

Verification

• cargo test --workspace green (default config — includes both new gates via ci.yml:53).
• cargo test -p synth-verify green (225 tests).
• cargo fmt --check + cargo clippy --workspace --all-targets -- -D warnings clean.

Bounded (named follow-up)

Reloc/overlap class only. The validator checks the resolved byte per reloc (matching the reference oracle); multi-byte accesses spanning an owning segment's packed-length boundary, all-addressing coverage, and the AArch64 / RV32 static bases are named follow-ups.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 84.18367% with 31 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-core/src/static_data_addr.rs	86.39%	23 Missing ⚠️
crates/synth-cli/src/main.rs	70.37%	8 Missing ⚠️

📢 Thoughts on this report? Let us know!