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

CLAUDE.md

@@ -152,13 +152,21 @@ frozen and oracle-gated every step:
 - **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). `VCR-VER-003` (#777, implemented
-  v0.46) is a per-compilation *static-data addressing* validator
+  v0.46; phase 2 v0.47) 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
+  bytes the packed `.data` serves equal the runtime-image bytes (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()`).
+  Phase 2 (#777 follow-ups): conservative multi-byte SPAN validation against
+  the shipped init blob on the mixed split (the staggered-overlap straddle is
+  refused with a span diagnostic); the self-contained `--cortex-m` #758 ROM
+  image is packed by a shared later-wins packer and validated unconditionally;
+  RV32 (single-base s11, ships no initializer image) warns loudly on nonzero
+  dropped initializer bytes (hard decline + initializer shipping = named
+  follow-up, held on the frozen control_step fixture); AArch64 is N/A (no
+  linear-memory ops in the integer subset).
 - **Track D (schedulability, #778):** `--emit-wcet` emits a SOUND static
   per-function worst-case cycle bound (`synth-wcet-v1` sidecar) as gale spar's
   T3/T4 `C_i` input — a bound, not a DWT observation. Loop-free functions get an

artifacts/verified-codegen-roadmap.yaml

@@ -1250,11 +1250,54 @@ artifacts:
       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.
+      PHASE 2 (v0.47, #777 follow-ups) — the phase-1 BOUNDED items, landed:
+      (5) MULTI-BYTE SPANS (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 emission extends the validated blob,
+      so the served side is the real artifact). Catches the staggered-overlap
+      straddle (addend byte correct, tail bytes runtime-owned by a LATER
+      segment — demonstrated live: the v0.46 binary compiled the synthetic
+      straddle fixture clean with packed seg_0 serving a4a5 where the runtime
+      image owns b0b1; phase 2 hard-fails it with `span byte +2`), the
+      4-align-padding-shifted crossing, and the init-region escape. DOCUMENTED
+      RESIDUE: a span byte NO segment covers at runtime (implicit-zero linmem)
+      is skipped — flagging it would hard-error the ubiquitous "pointer near a
+      sparse segment's end, narrow access" shape; exact checking needs a
+      recorded access width (named follow-up).
+      (6) SELF-CONTAINED --cortex-m (#758 ROM-copy): the dense flash image is
+      packed by the shared declaration-order packer (pack_rom_image) and
+      validated unconditionally against the reconstructed runtime image
+      (validate_served_image — every blob byte equals the later-wins byte,
+      zero in gaps; garbage-in-gap and first-wins packs are RED in the
+      permanent unit gate, the overwrite policy is an argument). The dense
+      layout (index = linmem offset) preserves spans/overlaps structurally, so
+      the straddle fixture that the mixed split refuses compiles CORRECTLY
+      here (e2e green gate).
+      (7) RV32 single-base scheme (s11 = __linear_memory_base, zeroed RAM):
+      the object ships NO static-data initializer image at all — probing found
+      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 nonzero un-served byte
+      (all-zero / zero-overwritten runtime images genuinely ARE served by
+      zeroed RAM and stay silent — a later-wins check, not a bytes grep).
+      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; the hard decline +
+      initializer shipping (the RV32 analogue of #758: linker-script
+      placement + startup copy) is the named follow-up.
+      (8) AArch64: N/A, verified — the -b aarch64 integer subset has no
+      linear-memory loads/stores (every memory op loud-declines at selection:
+      "unsupported wasm op for aarch64 subset"), so compiled code cannot
+      observe static data; there is nothing to validate.
+
+      BOUNDED (named follow-ups after phase 2): recorded per-reloc access
+      widths (removes the uncovered-span-byte tolerance and the conservative
+      8-byte widening); RV32 initializer shipping + hard decline (needs a
+      frozen-fixture refreeze ritual); all-addressing coverage (dynamic
+      base+index accesses that cross packed-segment boundaries at runtime are
+      out of static reach on the mixed split).
     status: implemented
     tags: [verification, addressing, relocation, soundness, mem757]
     links:
@@ -1272,13 +1315,22 @@ artifacts:
         - "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"
+        - "Phase 2: spanned reloc check against the SHIPPED init blob (straddle refused e2e, owner access green)"
+        - "Phase 2: #758 dense ROM image packed via pack_rom_image + validate_served_image (first-wins pack RED in the unit gate)"
+        - "Phase 2: RV32 zero-served-image check — nonzero dropped initializers WARN loudly; zero-overwritten silent"
       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.
+        regresses to a hard error under the .position() revert. Phase 2: the
+        staggered-overlap straddle fixture is REFUSED on the mixed split with
+        a span diagnostic (and compiles CORRECTLY self-contained); the #758
+        ROM image validates on every self-contained build (first-wins pack is
+        Mismatch in the unit gate); RV32 warns loudly on nonzero un-served
+        initializer bytes and stays silent on zero-served runtime images;
+        AArch64 is documented N/A (no linear-memory ops in the subset).
 
   # ---------------------------------------------------------------------------
   # Parallel ROI tracks (measured 2026-06-06): the allocator (VCR-RA-001) is the

claims.yaml

@@ -193,6 +193,20 @@ claims:
   # 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().
+  #
+  # Phase 2 (#777 follow-ups, v0.47): (a) SPANNED reloc check — the mixed split
+  # validates every runtime-covered byte of a conservatively-widened access
+  # (MAX_ACCESS_BYTES) against the SHIPPED packed init blob (the
+  # staggered-overlap straddle phase 1 silently miscompiled is now refused);
+  # (b) the self-contained #758 ROM image is packed by the shared
+  # declaration-order packer and validated unconditionally against the
+  # reconstructed runtime image; (c) the RV32 single-base path runs the
+  # zero-served-image check and WARNS LOUDLY on nonzero dropped initializer
+  # bytes (hard decline held on the CI-pinned RV32 frozen fixture — named
+  # follow-up); (d) AArch64 documented N/A (no linear-memory ops in the
+  # subset). The count-eq pins below hold the wiring UNCONDITIONAL: exactly
+  # one spanned-validator call on the mixed split, exactly one ROM-image and
+  # one RV32 served-image call.
   - 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"
@@ -206,6 +220,14 @@ claims:
         path: crates/synth-core/src/static_data_addr.rs
       - kind: file-exists
         path: crates/synth-cli/tests/vcr_ver_003_addr_777.rs
+      - kind: count-eq                       # phase 2: spanned check wired on the mixed split
+        pattern: 'validate_reloc_resolutions_spanned\('
+        glob: crates/synth-cli/src/main.rs
+        expect: 1
+      - kind: count-eq                       # phase 2: #758 ROM image + RV32 zero-served checks
+        pattern: 'validate_served_image\('
+        glob: crates/synth-cli/src/main.rs
+        expect: 2
 
   - id: SYNTH-VCR-SEL-001-STATUS
     doc: README.md

crates/synth-cli/src/main.rs

@@ -3402,6 +3402,42 @@ fn compile_all_exports(
         info!("Building AArch64 multi-function relocatable object (EM_AARCH64)");
         build_multi_func_aarch64_elf(&compiled_funcs)?
     } else if is_riscv {
+        // VCR-VER-003 phase 2 (#777): the RV32 single-base scheme (s11 =
+        // __linear_memory_base, zeroed RAM at reset) ships NO static-data
+        // initializer image — the object is `.text`-only, and neither the
+        // generated startup.c nor linker.ld carries the wasm data segments.
+        // Validate what zeroed RAM actually serves against the runtime image:
+        // any NONZERO later-wins byte is un-served (a load there returns 0x00
+        // instead of the initializer — the silent-drop analogue of #757).
+        // All-zero or zero-overwritten segments genuinely ARE served correctly
+        // and stay silent. This is a LOUD WARNING, not (yet) a hard error:
+        // the CI-pinned RV32 frozen fixture (control_step.wasm, which carries
+        // a nonzero active segment its differential never reads) freezes
+        // compile-success on this path; the hard-decline + initializer
+        // shipping (the RV32 analogue of #758) is the named follow-up.
+        let rv_segments: Vec<synth_core::static_data_addr::DataSegment> = all_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::ImageVerdict::Mismatch(mismatches) =
+            synth_core::static_data_addr::validate_served_image(&rv_segments, &[])
+        {
+            let first = &mismatches[0];
+            warn!(
+                "VCR-VER-003 (#777 phase 2): the RISC-V object ships NO \
+                 static-data initializer image — {} nonzero initializer byte(s) \
+                 (first: {}) will read as 0x00 from zeroed RAM at runtime. Any \
+                 load from those addresses is a SILENT MISCOMPILE; use the ARM \
+                 relocatable (--native-pointer-abi) or self-contained \
+                 (--cortex-m) paths for modules whose code reads its data \
+                 segments.",
+                mismatches.len(),
+                first.describe()
+            );
+        }
         info!("Building RISC-V multi-function relocatable object (EM_RISCV)");
         build_multi_func_riscv_elf(&compiled_funcs)?
     } else if has_external_relocations || relocatable {
@@ -4117,6 +4153,12 @@ fn build_relocatable_elf(
     // 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();
+    // #777 phase 2: the packed init region (segments at their 4-aligned packed
+    // offsets, NO globals slots yet) is built ONCE here — the span validator
+    // reads the same bytes the `.data` section will ship (the emission below
+    // extends this very blob with the globals slots), so the served side of
+    // the check is the real artifact, not a recompute.
+    let mut mixed_init_blob: Option<Vec<u8>> = None;
     if do_mixed_split {
         for (i, func) in funcs.iter().enumerate() {
             for reloc in &func.relocations {
@@ -4173,17 +4215,35 @@ fn build_relocatable_elf(
         // 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`.
+        //
+        // Phase 2 (#777): the check is SPANNED — beyond the addend byte, every
+        // runtime-covered byte a conservatively-widened access (up to
+        // MAX_ACCESS_BYTES; the reloc records no width) could read must equal
+        // what the packed init blob actually serves at that position. This
+        // catches the staggered-overlap straddle (addend byte correct, tail
+        // bytes runtime-owned by a LATER segment) and the packed-boundary
+        // crossing (4-align padding / next-declared segment / init-region
+        // escape) that phase 1's single-byte check accepted.
         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();
+        let (packed, globals_off, _data_size) = mixed_layout.as_ref().unwrap();
+        let mut init_blob = vec![0u8; *globals_off as usize];
+        for ((_off, d), &poff) in data_segments.iter().zip(packed.iter()) {
+            init_blob[poff as usize..poff as usize + d.len()].copy_from_slice(d);
+        }
         if let synth_core::static_data_addr::Verdict::Mismatch(mismatches) =
-            synth_core::static_data_addr::validate_reloc_resolutions(
+            synth_core::static_data_addr::validate_reloc_resolutions_spanned(
                 &val_segments,
                 &addr_resolutions,
+                &synth_core::static_data_addr::PackedInit {
+                    seg_packed_off: packed,
+                    bytes: &init_blob,
+                },
             )
         {
             let detail = mismatches
@@ -4193,12 +4253,15 @@ fn build_relocatable_elf(
                 .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}",
+                 relocation byte(s) disagree with the runtime linear-memory \
+                 image (this is the #757 silent-miscompile class; segments must \
+                 apply in declaration order, later-wins — a span mismatch means \
+                 an access starting in one packed segment would read stale or \
+                 non-adjacent bytes the runtime image does not hold):\n{detail}",
                 mismatches.len()
             );
         }
+        mixed_init_blob = Some(init_blob);
     }
 
     // #383 (VCR-MEM-001 layer-1 + #678 layer-2): shrink the [0, sp_init)
@@ -4432,17 +4495,19 @@ fn build_relocatable_elf(
             // #354: zero reservation -> NOBITS `.bss` (section 5),
             // `__synth_wasm_data` = 0; init segments packed into a small PROGBITS
             // `.data` (section 6), each under its own `__synth_wasm_seg_K`.
-            let (packed, globals_off, data_size) = mixed_layout.as_ref().unwrap();
+            let (_packed, globals_off, data_size) = mixed_layout.as_ref().unwrap();
             let bss = Section::new(".bss", ElfSectionType::NoBits)
                 .with_flags(SectionFlags::ALLOC | SectionFlags::WRITE)
                 .with_addr(0)
                 .with_align(4)
                 .with_size(reserved_extent);
             elf_builder.add_section(bss);
-            let mut blob = vec![0u8; *data_size as usize];
-            for ((_off, d), &poff) in data_segments.iter().zip(packed.iter()) {
-                blob[poff as usize..poff as usize + d.len()].copy_from_slice(d);
-            }
+            // #777 phase 2: ship the VALIDATED init blob (the span check above
+            // ran against these exact bytes), extended with the globals slots.
+            let mut blob = mixed_init_blob
+                .take()
+                .expect("mixed_init_blob is built whenever do_mixed_split");
+            blob.resize(*data_size as usize, 0);
             if let Some(ng) = &native_layout {
                 // #383: re-based SP slot when the shadow-stack shrink fired.
                 let globals = rebased_globals.as_ref().unwrap_or(&ng.globals);
@@ -5161,15 +5226,41 @@ fn build_multi_func_cortex_m_elf(
         );
     }
     let data_extent: u32 = data_extent_u64 as u32;
-    let data_rom_image: Vec<u8> = if data_extent == 0 {
-        Vec::new()
-    } else {
-        let mut blob = vec![0u8; data_extent as usize];
-        for (off, d) in data_segments {
-            blob[*off as usize..*off as usize + d.len()].copy_from_slice(d);
-        }
-        blob
-    };
+    // VCR-VER-003 phase 2 (#777): pack the dense image via the shared
+    // declaration-order (later-wins) packer, then VALIDATE it against the
+    // independently reconstructed runtime linear-memory image — every blob
+    // byte must equal the byte WASM instantiation leaves there (later
+    // segments overwrite earlier on overlap; gaps are zero). The dense layout
+    // (index = linmem offset) preserves spans and adjacency structurally, so
+    // this one obligation covers the whole self-contained static-data story.
+    // Unconditional; a mismatch is a compiler bug, never a module property.
+    let rom_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();
+    let data_rom_image: Vec<u8> =
+        synth_core::static_data_addr::pack_rom_image(&rom_segments, /* last_wins */ true);
+    debug_assert_eq!(data_rom_image.len() as u64, data_extent_u64);
+    if let synth_core::static_data_addr::ImageVerdict::Mismatch(mismatches) =
+        synth_core::static_data_addr::validate_served_image(&rom_segments, &data_rom_image)
+    {
+        let detail = mismatches
+            .iter()
+            .take(8)
+            .map(|m| format!("  {}", m.describe()))
+            .collect::<Vec<_>>()
+            .join("\n");
+        anyhow::bail!(
+            "VCR-VER-003: self-contained ROM data image validation FAILED — {} \
+             byte(s) of the #758 flash init image disagree with the runtime \
+             linear-memory image (segments applied in declaration order, \
+             later-wins). This is a compiler bug in the ROM packing:\n{detail}",
+            mismatches.len()
+        );
+    }
 
     // RAM layout — see the SRAM layout contract in this function's doc (#687).
     //