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

CLAUDE.md

@@ -146,7 +146,14 @@ frozen and oracle-gated every step:
   proposed.
 - **Track C (validation):** the differential oracles are CI-gated jobs
   (cmp-select, RV32 shift-fold/const-addr-fold, callee-saved, spill-frame,
-  symtab-based frozen-fixture differentials).
+  symtab-based frozen-fixture differentials). `VCR-VER-003` (#777, implemented
+  v0.46) is a per-compilation *static-data addressing* validator
+  (`synth_core::static_data_addr`): for every static-data reloc it proves the
+  byte the packed `.data` serves equals the runtime-image byte (overlapping
+  active segments applied later-wins), hard-erroring the compile on the #757
+  wrong-segment miscompile. Concrete byte-equality (not SMT), unconditional
+  (runs in the default `--features riscv` build), red-first gated (same
+  validator Mismatch on `.position()` / Consistent on `.rposition()`).
 - **Gate `VCR-VER-001`:** DEMONSTRATED (implemented, evidence in
   `scripts/repro/vcr_ver_001_gate.md`) — the v0.11.20 reciprocal-mult
   cost-gate was deleted outright (PR #322, differential bit-identical); the

artifacts/verified-codegen-roadmap.yaml

@@ -1186,6 +1186,100 @@ artifacts:
         validator obligation. Full auto-derivation for all classes is the
         documented exec-model follow-on.
 
+  - id: VCR-VER-003
+    type: sys-verification
+    title: "Static-data addressing VC catches the overlapping-segment wrong-segment miscompile (#757) at compile time on every module"
+    description: >
+      Make static-data-relocation resolution a checkable, per-compilation proof
+      obligation so the #757 silent miscompile — an overlapping active data
+      segment binding a static reloc to the WRONG (earlier) segment — can no
+      longer ship. #757 survived four releases (0.43.0/0.43.1/0.44.0/0.45.0)
+      because value-differential oracles are COVERAGE-limited: 7 synthetic
+      reconstructions were all green, and only gale's real fused gust:os node
+      (three active segments all at linmem 0x100000, string in the LAST) hit it.
+
+      Invariant (per compiled relocatable object, N 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. This lifts the post-hoc #757 differential
+      (scripts/repro/mem757_gale_differential.py) into a per-compilation
+      validator: a wrong-segment resolution FAILS at compile time on ANY module.
+
+      Concrete byte-equality, NOT fabricated SMT: there are no symbolic operands
+      (unlike VCR-VER-002's trap VCs), so the honest form is a direct comparison
+      against an independently reconstructed truth image. The runtime image is
+      derived ONLY from the segment list — never from the chosen K — so the
+      validator cannot be satisfied by mirroring the code under test
+      (mirror-pinning vacuity is structurally excluded).
+
+      STATUS implemented (v0.46). LANDED:
+      (1) synth_core::static_data_addr — validate_reloc_resolutions() over
+      DataSegment + the EMITTED RelocResolution (seg_index, addend), returning
+      Verdict {Consistent | Mismatch(Vec<AddrMismatch>)}. Lives in synth-core so
+      it runs UNCONDITIONALLY: the shipping build is `--features riscv`, NOT
+      `verify`, so a verify-gated check would stay dormant in exactly the build
+      that shipped #757. synth-verify::addr re-exports it (VCR-VER-002 structure
+      parity), single source, no mirror drift.
+      (2) Wired into the mixed-split reloc retargeting path (synth-cli main.rs):
+      the loop records the EMITTED (k, new_addend) per static-data reloc — never
+      recomputed — and hard-errors the compile (anyhow::bail!) on any Mismatch,
+      naming the symbol/addend/served/runtime bytes.
+      (3) RED-FIRST non-vacuity 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, goes
+      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 no source revert.
+      Plus partial-overlap-tail-wins, non-overlapping-both-consistent,
+      out-of-range-mismatch.
+      (4) 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(). That revert was demonstrated by hand for the
+      PR: compile FAILS with `func 9 reloc @ 0x250: __synth_wasm_seg_0+0x8 ->
+      linmem 0x100008 serves 0x02 but the runtime image owns 0x67` — exactly
+      gale's historical got=[2,0,0,0,..] = __synth_wasm_seg_0+8.
+
+      TRIGGER SCOPE: the validator runs 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). The #757 wrong-segment class exists ONLY on
+      that path, so "catches #757 on every module" holds: no module can exhibit
+      the wrong-segment miscompile uncaught. It is not a check that runs on every
+      compile in general.
+
+      BOUNDED (named follow-up): reloc/overlap class only. The validator checks
+      the RESOLVED byte per reloc (matching the reference oracle
+      mem757_gale_differential.py); a multi-byte access whose read spans an
+      owning segment's packed-length boundary is a named follow-up, as are
+      all-addressing coverage and the AArch64 / RV32 static bases.
+    status: implemented
+    tags: [verification, addressing, relocation, soundness, mem757]
+    links:
+      - type: verifies
+        target: VCR-001
+      - type: refines
+        target: VCR-VER-002
+    fields:
+      method: translation-validation
+      preconditions:
+        - "#354 mixed-split per-segment reloc retargeting (__synth_wasm_seg_K)"
+        - "#757 fix: overlapping addresses resolve to the last-declared owner (.rposition())"
+      steps:
+        - "synth_core::static_data_addr: runtime-image reconstruction + per-reloc byte-equality validator"
+        - "Wire the EMITTED (k, addend) into the mixed-split retarget loop; hard-error on Mismatch"
+        - "Red-first unit gate: Mismatch on .position(), Consistent on .rposition() (same validator, argument toggle)"
+        - "Durable e2e gate: real gale loom.wasm compiles exit-0; regresses to RED on the .position() revert"
+      pass-criteria: >
+        On any compiled relocatable object every static-data reloc resolves to
+        the runtime-correct byte (segments later-wins), else the compile fails.
+        The validator is Mismatch on the #757 wrong-segment (.position())
+        resolution and Consistent on the correct (.rposition()) one for an
+        overlapping-segment module; the real gale module compiles clean and
+        regresses to a hard error under the .position() revert.
+
   # ---------------------------------------------------------------------------
   # Parallel ROI tracks (measured 2026-06-06): the allocator (VCR-RA-001) is the
   # north-star but the const-remat is partly FORCED by the 9-register pool, so

claims.yaml

@@ -187,6 +187,26 @@ claims:
       - kind: file-exists
         path: crates/synth-verify/tests/trap_preservation.rs
 
+  # VCR-VER-003 (#777 / #757): per-compilation static-data addressing validator.
+  # Concrete byte-equality (NOT SMT): every static-data reloc resolves to the
+  # runtime-correct byte (active segments applied in declaration order,
+  # later-wins). In synth-core so it runs on EVERY compilation (default
+  # `--features riscv`, not `verify`). Non-vacuous red-first gate: same validator
+  # Mismatch on .position() (the #757 bug) / Consistent on .rposition().
+  - id: SYNTH-VCR-VER-003-STATUS
+    doc: artifacts/verified-codegen-roadmap.yaml
+    text: "Static-data addressing VC catches the overlapping-segment wrong-segment miscompile (#757) at compile time on every module"
+    evidence:
+      - kind: yaml-field
+        path: artifacts/verified-codegen-roadmap.yaml
+        id: VCR-VER-003
+        field: status
+        equals: implemented
+      - kind: file-exists
+        path: crates/synth-core/src/static_data_addr.rs
+      - kind: file-exists
+        path: crates/synth-cli/tests/vcr_ver_003_addr_777.rs
+
   - id: SYNTH-VCR-SEL-001-STATUS
     doc: README.md
     text: "increments 1–4 shipped default-on (`SYNTH_SEL_DSL`, opt-out `SYNTH_NO_SEL_DSL=1`)"

crates/synth-cli/src/main.rs

@@ -3942,6 +3942,12 @@ fn build_relocatable_elf(
     // by (func index, reloc offset) -> (new symbol, new addend). The addend C is
     // read from the in-place `.text` literal word (Abs32 is REL — `S + A`).
     let mut retarget: HashMap<(usize, u32), (String, i32)> = HashMap::new();
+    // VCR-VER-003 (#777 / #757): collect the retargeting the compiler ACTUALLY
+    // emits so a per-compilation validator can prove every static-data reloc
+    // resolves to the runtime-correct byte (segments applied later-wins). Built
+    // from the emitted `(k, new_addend)` — never recomputed — so the check
+    // consumes the real output and cannot be mirror-pinned vacuous.
+    let mut addr_resolutions: Vec<synth_core::static_data_addr::RelocResolution> = Vec::new();
     if do_mixed_split {
         for (i, func) in funcs.iter().enumerate() {
             for reloc in &func.relocations {
@@ -3981,9 +3987,49 @@ fn build_relocatable_elf(
                         (format!("__synth_wasm_seg_{k}"), new_addend),
                     );
                     all_code[pos..pos + 4].copy_from_slice(&new_addend.to_le_bytes());
+                    // VCR-VER-003: record the EMITTED (k, addend) for validation.
+                    addr_resolutions.push(synth_core::static_data_addr::RelocResolution {
+                        seg_index: k,
+                        addend: new_addend as u32,
+                        label: format!("func {i} reloc @ 0x{:x} (linmem 0x{c:x})", reloc.offset),
+                    });
                 }
             }
         }
+
+        // VCR-VER-003 (#777 / #757): per-compilation validation — prove every
+        // retargeted static-data reloc resolves to the runtime-correct byte
+        // (active data segments applied in declaration order, later-wins). The
+        // runtime image is reconstructed independently of the chosen segment, so
+        // a wrong-segment resolution (the #757 miscompile) FAILS here at compile
+        // time on ANY module. Unconditional — runs in the default `--features
+        // riscv` shipping build, not just `verify`.
+        let val_segments: Vec<synth_core::static_data_addr::DataSegment> = data_segments
+            .iter()
+            .map(|(off, d)| synth_core::static_data_addr::DataSegment {
+                linmem_off: *off,
+                bytes: d.clone(),
+            })
+            .collect();
+        if let synth_core::static_data_addr::Verdict::Mismatch(mismatches) =
+            synth_core::static_data_addr::validate_reloc_resolutions(
+                &val_segments,
+                &addr_resolutions,
+            )
+        {
+            let detail = mismatches
+                .iter()
+                .map(|m| format!("  {}", m.describe()))
+                .collect::<Vec<_>>()
+                .join("\n");
+            anyhow::bail!(
+                "VCR-VER-003: static-data addressing validation FAILED — {} \
+                 relocation(s) resolve to the wrong overlapping-segment byte \
+                 (this is the #757 silent-miscompile class; segments must apply \
+                 in declaration order, later-wins):\n{detail}",
+                mismatches.len()
+            );
+        }
     }
 
     // #383 (VCR-MEM-001 layer-1 + #678 layer-2): shrink the [0, sp_init)

crates/synth-cli/tests/vcr_ver_003_addr_777.rs

@@ -0,0 +1,84 @@
+//! VCR-VER-003 (#777 / #757) — the static-data addressing validator is wired
+//! UNCONDITIONALLY into the mixed-split reloc path (`main.rs`, default
+//! `--features riscv` build, no `verify` feature). It proves every retargeted
+//! static-data relocation resolves to the runtime-correct byte (active data
+//! segments applied in declaration order, later-wins).
+//!
+//! This is the DURABLE end-to-end tripwire for the #757 miscompile. gale's real
+//! fused `gust:os` node (`scripts/repro/mem757_gale/loom.wasm`) declares three
+//! active segments all at linmem `0x100000`; the string lives in the last
+//! (`seg_2`) but a `.position()` (first-match) retargeting bound its reads to
+//! `seg_0`'s stale consts. Because the validator now runs on every compile, this
+//! test goes RED precisely when someone reverts the fix (`main.rs`
+//! `.rposition()`→`.position()`) — that regression was demonstrated by hand in
+//! the VCR-VER-003 PR (compile errored `func 9 reloc @ 0x250 __synth_wasm_seg_0
+//! +0x8 serves 0x02 but runtime owns 0x67`); this test makes the GREEN side
+//! permanent so the regression cannot land silently.
+//!
+//! The synthetic 3-overlap DISCRIMINATION (RED on `.position()`, GREEN on
+//! `.rposition()`, same validator) is a permanent unit test in
+//! `synth_core::static_data_addr` (`red_on_first_match_green_on_last_match`);
+//! keeping the REAL module here honours the "synthetic reconstructions were all
+//! green — the real module must live in CI" lesson (#757 survived 7 synthetic
+//! shapes).
+
+use std::path::PathBuf;
+use std::process::Command;
+
+fn synth() -> &'static str {
+    env!("CARGO_BIN_EXE_synth")
+}
+
+fn repro(name: &str) -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("../..")
+        .join("scripts/repro")
+        .join(name)
+}
+
+/// The real gale overlapping-segment module compiles cleanly: the addressing
+/// validator passes because the shipped `.rposition()` resolves the overlap to
+/// the last-declared owner. A regression to `.position()` makes this compile
+/// FAIL (VCR-VER-003 hard-error), so this GREEN is the #757 regression gate.
+#[test]
+fn gale_overlapping_segments_compile_clean() {
+    let fixture = repro("mem757_gale/loom.wasm");
+    assert!(
+        fixture.exists(),
+        "missing gale fixture {}",
+        fixture.display()
+    );
+    let out = std::env::temp_dir().join("vcr_ver_003_gale.o");
+    let output = Command::new(synth())
+        .args([
+            "compile",
+            fixture.to_str().unwrap(),
+            "--target",
+            "cortex-m3",
+            "--all-exports",
+            "--relocatable",
+            "--native-pointer-abi",
+            "--shadow-stack-size",
+            "2048",
+            "-o",
+            out.to_str().unwrap(),
+        ])
+        .output()
+        .expect("run synth");
+
+    let stderr = String::from_utf8_lossy(&output.stderr);
+    assert!(
+        output.status.success(),
+        "gale module must compile clean under the shipped .rposition() \
+         retargeting — VCR-VER-003 rejected it, which means the overlapping \
+         segments resolved to the WRONG segment (the #757 miscompile has \
+         regressed):\n{stderr}"
+    );
+    // Sanity: the validator must NOT have fired on the correct path.
+    assert!(
+        !stderr.contains("VCR-VER-003"),
+        "VCR-VER-003 must be silent on the runtime-correct resolution:\n{stderr}"
+    );
+    assert!(out.exists(), "expected a relocatable .o output");
+    let _ = std::fs::remove_file(&out);
+}

crates/synth-core/src/lib.rs

@@ -12,6 +12,7 @@ pub mod ir;
 pub mod provenance;
 pub mod safety_manifest;
 pub mod sbom;
+pub mod static_data_addr;
 pub mod target;
 pub mod wasm_decoder;
 pub mod wasm_op;