From 897cac77c479e93ba5f1b7abd172659a18bd1d0a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 06:23:12 +0200 Subject: [PATCH 1/5] feat(#777-ph2): span + dense-image static-data validators in synth-core VCR-VER-003 phase 2 core: validate_reloc_resolutions_spanned (conservative MAX_ACCESS_BYTES span per reloc against the EMITTED packed init blob, with the documented unknown-width uncovered-byte tolerance), pack_rom_image / validate_served_image (dense #758 ROM image + the RV32 zero-served shape), red-first unit gates per class (phase-1-green-but-span-red staggered overlap, padding-shifted crossing, init-region escape, first-wins vs last-wins ROM pack, zero-served nonzero drop vs zero-overwrite green). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-core/src/static_data_addr.rs | 571 +++++++++++++++++++++- crates/synth-verify/src/addr.rs | 4 +- 2 files changed, 571 insertions(+), 4 deletions(-) diff --git a/crates/synth-core/src/static_data_addr.rs b/crates/synth-core/src/static_data_addr.rs index f59d92ef..60dd6076 100644 --- a/crates/synth-core/src/static_data_addr.rs +++ b/crates/synth-core/src/static_data_addr.rs @@ -42,9 +42,48 @@ //! side never touches `K`, so the validator cannot be satisfied by mirroring //! the code under test (the mirror-pinning vacuity mode is structurally //! excluded). `synth-verify` re-exports this module for the VCR-VER-003 tests. +//! +//! # Phase 2 (#777 follow-ups) +//! +//! Phase 1 validated the single resolved **addend byte** per reloc. Phase 2 +//! extends coverage to the named follow-up classes: +//! +//! 1. **Multi-byte access spans** ([`validate_reloc_resolutions_spanned`]): +//! a reloc whose addend byte is runtime-correct can still mis-serve TAIL +//! bytes — an i32/i64 load starting in segment `K` whose span crosses into +//! a range a LATER-declared segment owns at runtime (staggered overlap), or +//! crosses `K`'s packed end into 4-align padding / the next *declared* +//! (not next *linmem*) segment. The access width is not recorded on +//! [`crate::backend::CodeRelocation`] (the Abs32 literal is a pointer; its +//! consumers are ldrb/ldrh/ldr/ldrd), so the span is validated +//! conservatively out to [`MAX_ACCESS_BYTES`] with one deliberate +//! tolerance: a span byte whose runtime address NO segment covers is +//! skipped (implicit-zero linear memory — flagging it would hard-error the +//! ubiquitous "pointer near the end of a sparse segment, narrow access" +//! shape). A span byte that IS runtime-covered must match what the packed +//! blob actually serves at that position, byte-for-byte, so the served +//! side reads the EMITTED init blob ([`PackedInit`]) — never a recompute. +//! 2. **Dense served images** ([`validate_served_image`] / +//! [`pack_rom_image`]): the self-contained `--cortex-m` ROM-copy layout +//! (#758) serves linear memory from ONE dense flash blob copied to RAM at +//! reset — index = linmem offset, so spans/overlaps are structurally +//! preserved and the whole obligation reduces to "every blob byte equals +//! the runtime image byte (later-wins, zero elsewhere)". The same function +//! with an EMPTY image validates the RISC-V single-base scheme, where the +//! object ships NO initializer bytes at all and zeroed RAM serves every +//! address: any nonzero runtime-image byte is then a served/runtime +//! mismatch (the silent initializer-drop). +//! 3. **AArch64: N/A** — the `-b aarch64` integer subset has no linear-memory +//! loads/stores (every memory op loud-declines at selection), so compiled +//! code cannot observe static data; there is nothing to validate. use std::collections::HashMap; +/// The widest scalar linear-memory access synth can emit (i64.load / +/// i64.store — there is no v128 support on these paths). Conservative span +/// bound used when a reloc's true access width is unknown. +pub const MAX_ACCESS_BYTES: u32 = 8; + /// One active WASM data segment: its linear-memory offset and its bytes, in /// declaration order. The packed `.data` blob stores these bytes verbatim /// (4-aligned per segment) under `__synth_wasm_seg_K`; index `K` in the segment @@ -93,19 +132,32 @@ pub struct AddrMismatch { pub seg_index: usize, /// The emitted addend. pub addend: u32, - /// The original linear-memory access address (`seg[K].off + addend`). + /// The original linear-memory access address of the OFFENDING byte + /// (`seg[K].off + addend + span_byte`). pub access_addr: u32, - /// The byte the packed `.data` serves (`seg[K].bytes[addend]`). + /// The byte the packed `.data` serves at that position. pub served: u8, /// The byte the runtime image holds at `access_addr` (the truth). pub runtime: u8, + /// Which byte of the (potentially multi-byte) access diverges: 0 = the + /// addend byte itself (the phase-1 check), 1..[`MAX_ACCESS_BYTES`] = a + /// tail byte of a conservatively-widened span (phase 2). + pub span_byte: u32, } impl AddrMismatch { /// A human-readable one-line diagnostic for the compile-time error. pub fn describe(&self) -> String { + let span = if self.span_byte == 0 { + String::new() + } else { + format!( + " (span byte +{} of a possibly {}-byte access)", + self.span_byte, MAX_ACCESS_BYTES + ) + }; format!( - "{}: __synth_wasm_seg_{}+0x{:x} -> linmem 0x{:x} serves 0x{:02x} but \ + "{}: __synth_wasm_seg_{}+0x{:x} -> linmem 0x{:x}{span} serves 0x{:02x} but \ the runtime image (segments applied later-wins) owns 0x{:02x}", self.label, self.seg_index, self.addend, self.access_addr, self.served, self.runtime ) @@ -148,6 +200,7 @@ pub fn validate_reloc_resolutions( access_addr: 0, served: 0, runtime: 0, + span_byte: 0, }); continue; }; @@ -161,6 +214,7 @@ pub fn validate_reloc_resolutions( access_addr, served: 0, runtime: 0, + span_byte: 0, }); continue; }; @@ -176,6 +230,7 @@ pub fn validate_reloc_resolutions( access_addr, served, runtime: 0, + span_byte: 0, }); continue; }; @@ -187,6 +242,7 @@ pub fn validate_reloc_resolutions( access_addr, served, runtime: runtime_byte, + span_byte: 0, }); } } @@ -223,6 +279,212 @@ pub fn resolve_owner(segments: &[DataSegment], c: u32, last_wins: bool) -> Optio }) } +/// The EMITTED packed-`.data` init region of the #354 mixed split: each +/// segment's bytes at its 4-aligned packed offset, in declaration order, +/// EXCLUDING the trailing `__synth_globals` slots. Both fields are read back +/// from what the compiler actually laid out / filled — the validator never +/// recomputes the packing (that would mirror-pin the check). +#[derive(Clone, Debug)] +pub struct PackedInit<'a> { + /// Packed offset of each segment inside the init region (declaration + /// order, parallel to the segment list). + pub seg_packed_off: &'a [u32], + /// The init-region bytes the object will ship (segments + 4-align + /// padding). A span byte served from BEYOND this region (the globals + /// slots, or past the blob) can never be a linear-memory byte. + pub bytes: &'a [u8], +} + +/// Phase-2 (#777) per-compilation addressing gate: the phase-1 addend-byte +/// check PLUS a conservative multi-byte span check per reloc. +/// +/// For every emitted resolution `(K, A)` and every span byte +/// `j in 0..`[`MAX_ACCESS_BYTES`]: +/// +/// - the byte SERVED is read from the emitted init blob at +/// `packed.seg_packed_off[K] + A + j` (the real artifact — for `j = 0` this +/// also pins the blob fill itself: a blob that doesn't hold `seg[K].bytes` +/// verbatim fails here); +/// - the byte OWED is the runtime image at `seg[K].off + A + j` (segments +/// applied in declaration order, later-wins, independent of `K`). +/// +/// `j = 0` keeps phase-1 semantics exactly (a missing byte on either side is +/// a broken retargeting → mismatch). For `j > 0` the access width is unknown +/// (see the module docs), so one tolerance applies: when NO segment covers +/// the runtime address, the byte is implicit-zero linear memory and the span +/// byte is SKIPPED — a wide access genuinely reaching there would read packed +/// neighbours instead of zeros, but flagging it would hard-error the common +/// "pointer near a sparse segment's end, narrow access" shape; exact checking +/// of that residue needs a recorded access width (named follow-up). When the +/// runtime address IS covered by some segment, the served byte must match — +/// including bytes past `K`'s packed end (4-align padding or the next +/// *declared* segment) and bytes that escape the init region entirely (both +/// are exactly how a straddling access mis-serves). +pub fn validate_reloc_resolutions_spanned( + segments: &[DataSegment], + resolutions: &[RelocResolution], + packed: &PackedInit<'_>, +) -> Verdict { + let runtime = runtime_image(segments); + let mut bad = Vec::new(); + // Phase-1 addend-byte check (byte 0, strict on both sides). + if let Verdict::Mismatch(m) = validate_reloc_resolutions(segments, resolutions) { + bad.extend(m); + } + for r in resolutions { + let Some(seg) = segments.get(r.seg_index) else { + continue; // already reported by the phase-1 pass + }; + let Some(&poff) = packed.seg_packed_off.get(r.seg_index) else { + continue; // impossible when layout and segments are parallel + }; + for j in 1..MAX_ACCESS_BYTES { + let access_addr = seg.linmem_off.wrapping_add(r.addend).wrapping_add(j); + // Unknown-width tolerance: runtime-uncovered ⇒ implicit zero ⇒ skip. + let Some(&runtime_byte) = runtime.get(&access_addr) else { + continue; + }; + let p = poff as usize + r.addend as usize + j as usize; + // Served byte: the emitted blob, or "not linear memory at all" + // when the span escapes the init region (globals slots / past the + // blob) — that escape can never serve a runtime-covered byte. + let served = packed.bytes.get(p).copied(); + if served != Some(runtime_byte) { + bad.push(AddrMismatch { + label: r.label.clone(), + seg_index: r.seg_index, + addend: r.addend, + access_addr, + served: served.unwrap_or(0), + runtime: runtime_byte, + span_byte: j, + }); + } + } + } + if bad.is_empty() { + Verdict::Consistent + } else { + Verdict::Mismatch(bad) + } +} + +/// The verdict of a dense served-image gate ([`validate_served_image`]). +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum ImageVerdict { + /// Every linear-memory byte the image (or zeroed RAM) serves equals the + /// runtime image byte. + Consistent, + /// At least one served byte disagrees with the runtime image. + Mismatch(Vec), +} + +/// One dense-image byte that disagrees with the runtime image. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct ImageMismatch { + /// The linear-memory address (= image index) of the offending byte. + pub addr: u32, + /// The byte the image serves (0 when the image doesn't reach `addr` — + /// zeroed RAM / no initializer shipped). + pub served: u8, + /// The byte the runtime image holds there (the truth). + pub runtime: u8, +} + +impl ImageMismatch { + /// A human-readable one-line diagnostic. + pub fn describe(&self) -> String { + format!( + "linmem 0x{:x} serves 0x{:02x} but the runtime image (segments \ + applied later-wins) owns 0x{:02x}", + self.addr, self.served, self.runtime + ) + } +} + +/// Total extent of the runtime image: `max(off + len)` over the segments +/// (u64, so a hostile `off + len` cannot wrap — callers bound-check against +/// the linear-memory size before packing). +pub fn image_extent(segments: &[DataSegment]) -> u64 { + segments + .iter() + .map(|s| s.linmem_off as u64 + s.bytes.len() as u64) + .max() + .unwrap_or(0) +} + +/// Pack the #758 dense ROM init image: a `[0, extent)` blob with every active +/// segment placed AT its linmem offset. `last_wins = true` applies them in +/// declaration order (WASM instantiation semantics — later segments overwrite +/// earlier on overlap); `last_wins = false` applies them in REVERSE order +/// (first-wins — the synthetic miscompile the red-first gate toggles, phase +/// 1's `resolve_owner` pattern). The caller must have bound-checked +/// [`image_extent`] against the linear-memory size (u32 + usize safe here +/// only after that check). +pub fn pack_rom_image(segments: &[DataSegment], last_wins: bool) -> Vec { + let mut blob = vec![0u8; image_extent(segments) as usize]; + let place = |blob: &mut Vec, s: &DataSegment| { + let at = s.linmem_off as usize; + blob[at..at + s.bytes.len()].copy_from_slice(&s.bytes); + }; + if last_wins { + for s in segments { + place(&mut blob, s); + } + } else { + for s in segments.iter().rev() { + place(&mut blob, s); + } + } + blob +} + +/// Dense served-image gate: for every address in `[0, image_extent)`, the byte +/// SERVED — `image[addr]`, or `0` when the image doesn't reach `addr` (zeroed +/// RAM; an empty `image` models a target that ships NO initializer bytes, the +/// RISC-V single-base scheme) — must equal the runtime image byte (segments +/// applied in declaration order, later-wins; implicit zero where uncovered). +/// +/// The truth side is reconstructed only from the segment list, never from the +/// image, so the gate cannot be satisfied by mirroring the packing code. +pub fn validate_served_image(segments: &[DataSegment], image: &[u8]) -> ImageVerdict { + let runtime = runtime_image(segments); + let mut bad = Vec::new(); + // Every image byte must equal the runtime byte (covered ⇒ later-wins + // segment byte; uncovered ⇒ implicit zero, so initializer garbage in a + // gap is caught too). + for (addr, &served) in image.iter().enumerate() { + let owed = runtime.get(&(addr as u32)).copied().unwrap_or(0); + if served != owed { + bad.push(ImageMismatch { + addr: addr as u32, + served, + runtime: owed, + }); + } + } + // Every runtime byte BEYOND the image is served by zeroed RAM, so any + // nonzero one is un-served (the shipped-no-initializer mismatch). Walk + // the covered addresses only — uncovered beyond-image bytes are 0 == 0. + let mut beyond: Vec<(u32, u8)> = runtime + .into_iter() + .filter(|&(addr, owed)| addr as u64 >= image.len() as u64 && owed != 0) + .collect(); + beyond.sort_unstable(); + for (addr, owed) in beyond { + bad.push(ImageMismatch { + addr, + served: 0, + runtime: owed, + }); + } + if bad.is_empty() { + ImageVerdict::Consistent + } else { + ImageVerdict::Mismatch(bad) + } +} + #[cfg(test)] mod tests { use super::*; @@ -354,6 +616,309 @@ mod tests { ); } + /// Pack the mixed-split init region for tests exactly the way main.rs + /// lays it out: each segment 4-aligned, declaration order. + fn mixed_pack(segments: &[DataSegment]) -> (Vec, Vec) { + let mut offs = Vec::with_capacity(segments.len()); + let mut cur = 0u32; + for s in segments { + cur = cur.next_multiple_of(4); + offs.push(cur); + cur += s.bytes.len() as u32; + } + let mut blob = vec![0u8; cur as usize]; + for (s, &o) in segments.iter().zip(offs.iter()) { + blob[o as usize..o as usize + s.bytes.len()].copy_from_slice(&s.bytes); + } + (offs, blob) + } + + /// PHASE-2 RED-FIRST (span class, the #777 follow-up): a STAGGERED overlap + /// — seg_1 overwrites only the TAIL of seg_0's range — with a reloc whose + /// addend byte is runtime-correct (owned by seg_0) but whose i32-wide span + /// crosses into seg_1's runtime-owned bytes. The phase-1 addend-byte + /// validator is GREEN on it (that is the hole this class names); the + /// spanned validator must be RED, flagging the exact tail byte. A spanned + /// validator green here would be vacuous. + #[test] + fn phase1_green_but_span_red_on_staggered_overlap() { + let segs = vec![ + DataSegment { + linmem_off: 0x10004, + bytes: vec![0xA0, 0xA1, 0xA2, 0xA3, 0xA4, 0xA5, 0xA6, 0xA7], + }, + // Staggered: overwrites [0x10008, 0x1000C) — seg_0's tail. + DataSegment { + linmem_off: 0x10008, + bytes: vec![0xB0, 0xB1, 0xB2, 0xB3], + }, + ]; + // Reloc at 0x10006: owner is seg_0 under the CORRECT .rposition() + // (seg_1 does not contain 0x10006). An i32 load spans 0x10006..0x1000A + // — bytes +2/+3 are seg_1's at runtime, seg_0's stale in the pack. + let r = resolve_owner(&segs, 0x10006, true).unwrap(); + assert_eq!(r.seg_index, 0, "correct owner of the addend byte is seg_0"); + // Phase-1 (addend byte only) is GREEN — the documented hole. + assert_eq!( + validate_reloc_resolutions(&segs, std::slice::from_ref(&r)), + Verdict::Consistent, + "phase 1 must accept the addend byte (it IS runtime-correct)" + ); + // Phase-2 spanned is RED at span byte +2. + let (offs, blob) = mixed_pack(&segs); + let packed = PackedInit { + seg_packed_off: &offs, + bytes: &blob, + }; + match validate_reloc_resolutions_spanned(&segs, std::slice::from_ref(&r), &packed) { + Verdict::Mismatch(m) => { + assert_eq!(m[0].span_byte, 2, "first divergent byte is +2"); + assert_eq!(m[0].access_addr, 0x10008); + assert_eq!(m[0].served, 0xA4, "packed seg_0 serves its stale byte"); + assert_eq!(m[0].runtime, 0xB0, "runtime image owns seg_1's byte"); + } + Verdict::Consistent => { + panic!("VACUOUS: spanned validator accepted a straddling stale-tail access") + } + } + } + + /// Linmem-ADJACENT segments whose packed layout PRESERVES adjacency + /// (4-aligned length, next declaration) — a span crossing the boundary is + /// served the right bytes, so the spanned validator must stay GREEN (no + /// false red on the benign crossing). + #[test] + fn span_green_on_adjacency_preserving_crossing() { + let segs = vec![ + DataSegment { + linmem_off: 0x100, + bytes: vec![1, 2, 3, 4], + }, + DataSegment { + linmem_off: 0x104, + bytes: vec![5, 6, 7, 8], + }, + ]; + let (offs, blob) = mixed_pack(&segs); + let packed = PackedInit { + seg_packed_off: &offs, + bytes: &blob, + }; + let r = resolve_owner(&segs, 0x102, true).unwrap(); + assert_eq!(r.seg_index, 0); + assert_eq!( + validate_reloc_resolutions_spanned(&segs, &[r], &packed), + Verdict::Consistent, + "packed adjacency == linmem adjacency: the crossing serves the right bytes" + ); + } + + /// Linmem-adjacent segments whose packed layout BREAKS adjacency (seg_0's + /// length is not 4-aligned, so the pack inserts padding the linear memory + /// doesn't have): a span crossing the boundary reads pad zeros instead of + /// the next segment's bytes — RED. + #[test] + fn span_red_on_padding_shifted_crossing() { + let segs = vec![ + DataSegment { + linmem_off: 0x100, + bytes: vec![1, 2, 3], // len 3 → packed pads to 4 + }, + // Linmem-adjacent at 0x103; packed at offset 4 (shifted by 1). + DataSegment { + linmem_off: 0x103, + bytes: vec![5, 6, 7, 8], + }, + ]; + let (offs, blob) = mixed_pack(&segs); + let packed = PackedInit { + seg_packed_off: &offs, + bytes: &blob, + }; + let r = resolve_owner(&segs, 0x101, true).unwrap(); + assert_eq!(r.seg_index, 0); + match validate_reloc_resolutions_spanned(&segs, &[r], &packed) { + Verdict::Mismatch(m) => { + // +2 = 0x103: runtime owns seg_1's first byte (5); the pack + // serves its own pad byte (0). + assert_eq!(m[0].span_byte, 2); + assert_eq!(m[0].access_addr, 0x103); + assert_eq!(m[0].served, 0, "the pack serves 4-align padding"); + assert_eq!(m[0].runtime, 5); + } + Verdict::Consistent => panic!("VACUOUS: padding-shifted crossing accepted"), + } + } + + /// The unknown-width tolerance: a reloc near the end of a SPARSE segment + /// (no segment covers the bytes beyond it) must stay GREEN — the span + /// bytes are implicit-zero linear memory and the common shape is a narrow + /// access. This is the documented residue, not a bug. + #[test] + fn span_green_on_sparse_tail() { + let segs = vec![ + DataSegment { + linmem_off: 0x100, + bytes: vec![1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12], + }, + // Far away; between them is implicit-zero linmem. + DataSegment { + linmem_off: 0x400, + bytes: vec![0xFF; 4], + }, + ]; + let (offs, blob) = mixed_pack(&segs); + let packed = PackedInit { + seg_packed_off: &offs, + bytes: &blob, + }; + // Last word of seg_0: the conservative 8-byte span runs past the end + // into uncovered linmem — skipped, not flagged. + let r = resolve_owner(&segs, 0x108, true).unwrap(); + assert_eq!(r.seg_index, 0); + assert_eq!( + validate_reloc_resolutions_spanned(&segs, &[r], &packed), + Verdict::Consistent, + "uncovered span bytes are implicit-zero linmem — must not false-red" + ); + } + + /// A span that escapes the init region entirely (into the globals slots / + /// past the blob) while the runtime address IS segment-covered: RED — the + /// pack cannot serve that byte at all. Shape: the LAST-declared segment is + /// shorter than an earlier one at the same base, so bytes beyond its end + /// are runtime-owned by the earlier segment but packed nowhere after it. + #[test] + fn span_red_on_init_region_escape() { + let segs = vec![ + DataSegment { + linmem_off: 0x100, + bytes: vec![0x11; 8], // covers [0x100, 0x108) + }, + DataSegment { + linmem_off: 0x100, + bytes: vec![0x22; 4], // last-declared owner of [0x100, 0x104) + }, + ]; + let (offs, blob) = mixed_pack(&segs); + assert_eq!(blob.len(), 12, "seg_1 is the final packed segment"); + let packed = PackedInit { + seg_packed_off: &offs, + bytes: &blob, + }; + // 0x102 is owned by seg_1 (last); its span bytes +2/+3 (0x104/0x105) + // are runtime-owned by seg_0 (0x11) but lie past seg_1's packed end = + // past the whole init region. + let r = resolve_owner(&segs, 0x102, true).unwrap(); + assert_eq!(r.seg_index, 1); + match validate_reloc_resolutions_spanned(&segs, &[r], &packed) { + Verdict::Mismatch(m) => { + assert_eq!(m[0].span_byte, 2); + assert_eq!(m[0].access_addr, 0x104); + assert_eq!(m[0].runtime, 0x11); + } + Verdict::Consistent => panic!("VACUOUS: init-region escape accepted"), + } + } + + /// ROM-image RED-FIRST (self-contained class, phase 1's `resolve_owner` + /// pattern — the overwrite policy is an ARGUMENT): on an overlapping + /// module the SAME dense-image validator must be RED on the first-wins + /// pack (`last_wins = false`, the synthetic miscompile) and GREEN on the + /// declaration-order pack (`last_wins = true`, WASM instantiation + /// semantics). Green on both would be vacuous. + #[test] + fn rom_image_red_on_first_wins_green_on_last_wins() { + let segs = overlapping_segments(); + let wrong = pack_rom_image(&segs, false); + match validate_served_image(&segs, &wrong) { + ImageVerdict::Mismatch(m) => { + // The classic #757 byte: offset 8 must be seg_2's 'u', but the + // first-wins image left seg_0's 0xAA there. + let at8 = m.iter().find(|x| x.addr == 0x100008).expect("addr 8"); + assert_eq!(at8.served, 0xAA); + assert_eq!(at8.runtime, b'u'); + } + ImageVerdict::Consistent => { + panic!("VACUOUS: dense-image validator accepted a first-wins pack") + } + } + let right = pack_rom_image(&segs, true); + assert_eq!( + validate_served_image(&segs, &right), + ImageVerdict::Consistent, + "declaration-order (later-wins) pack must validate" + ); + } + + /// A dense image with initializer garbage in an uncovered GAP is a + /// mismatch (runtime linmem is zero there), and a truncated image whose + /// missing tail is all-zero at runtime is fine (zeroed RAM serves it). + #[test] + fn rom_image_gap_garbage_red_zero_tail_green() { + let segs = vec![ + DataSegment { + linmem_off: 0, + bytes: vec![1, 2], + }, + DataSegment { + linmem_off: 8, + bytes: vec![0, 0, 0, 0], + }, + ]; + // Garbage at uncovered addr 4. + let mut img = pack_rom_image(&segs, true); + img[4] = 0xCC; + assert!(matches!( + validate_served_image(&segs, &img), + ImageVerdict::Mismatch(_) + )); + // Image truncated to the nonzero prefix: the all-zero tail (gap + + // zero segment) is served by zeroed RAM — consistent. + assert_eq!( + validate_served_image(&segs, &[1, 2]), + ImageVerdict::Consistent + ); + } + + /// RISC-V single-base shape: the object ships NO initializer image + /// (`image = &[]`, zeroed RAM serves everything). Nonzero segment bytes + /// are un-served (RED, the silent initializer-drop); an all-zero segment + /// — or an earlier nonzero byte OVERWRITTEN to zero by a later segment — + /// is served correctly by zeroed RAM (GREEN). The overwrite case keeps + /// this non-vacuous as a later-wins check, not a "any nonzero data" grep. + #[test] + fn zero_served_image_red_on_nonzero_green_on_zeroed() { + let nonzero = vec![DataSegment { + linmem_off: 16, + bytes: vec![1, 2, 3, 4], + }]; + match validate_served_image(&nonzero, &[]) { + ImageVerdict::Mismatch(m) => { + assert_eq!(m[0].addr, 16); + assert_eq!(m[0].served, 0); + assert_eq!(m[0].runtime, 1); + } + ImageVerdict::Consistent => panic!("VACUOUS: dropped nonzero initializer accepted"), + } + let zeroed = vec![ + DataSegment { + linmem_off: 16, + bytes: vec![1, 2, 3, 4], + }, + // Later segment overwrites the nonzero bytes with zeros: the + // runtime image is all-zero, so zeroed RAM serves it correctly. + DataSegment { + linmem_off: 16, + bytes: vec![0, 0, 0, 0], + }, + ]; + assert_eq!( + validate_served_image(&zeroed, &[]), + ImageVerdict::Consistent + ); + } + /// Out-of-range resolution (a broken retargeting) is a mismatch. #[test] fn out_of_range_is_mismatch() { diff --git a/crates/synth-verify/src/addr.rs b/crates/synth-verify/src/addr.rs index c458f3d9..f8d6193c 100644 --- a/crates/synth-verify/src/addr.rs +++ b/crates/synth-verify/src/addr.rs @@ -14,5 +14,7 @@ //! tests. pub use synth_core::static_data_addr::{ - AddrMismatch, DataSegment, RelocResolution, Verdict, resolve_owner, validate_reloc_resolutions, + AddrMismatch, DataSegment, ImageMismatch, ImageVerdict, MAX_ACCESS_BYTES, PackedInit, + RelocResolution, Verdict, image_extent, pack_rom_image, resolve_owner, + validate_reloc_resolutions, validate_reloc_resolutions_spanned, validate_served_image, }; From 4d09f696b3e5b284926105e716881a4fbe393a09 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 06:28:17 +0200 Subject: [PATCH 2/5] feat(#777-ph2): wire span/ROM-image/RV32 static-data validation into the compile paths MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - mixed-split: validate_reloc_resolutions_spanned against the SHIPPED init blob (built once, validated, then extended with globals and emitted) — the staggered-overlap straddle phase 1 silently miscompiled now hard-fails - self-contained --cortex-m: #758 ROM image packed via shared pack_rom_image (declaration-order later-wins) + unconditional dense-image validation - RV32: unconditional zero-served-image check — nonzero dropped initializer bytes WARN LOUDLY (hard decline held: control_step.wasm frozen fixture pins compile-success; initializer shipping is the named follow-up) - e2e gates in vcr_ver_003_addr_777.rs: straddle refused w/ span diagnostic, owner access green, self-contained straddle green + ROM image present, RV32 nonzero warns / zero-overwritten silent Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-cli/src/main.rs | 127 +++++++++-- .../synth-cli/tests/vcr_ver_003_addr_777.rs | 204 ++++++++++++++++++ 2 files changed, 313 insertions(+), 18 deletions(-) diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index 1df8a7b1..4babdabc 100644 --- a/crates/synth-cli/src/main.rs +++ b/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 = 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 = 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> = None; if do_mixed_split { for (i, func) in funcs.iter().enumerate() { for reloc in &func.relocations { @@ -4173,6 +4215,15 @@ 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 = data_segments .iter() .map(|(off, d)| synth_core::static_data_addr::DataSegment { @@ -4180,10 +4231,19 @@ fn build_relocatable_elf( 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 = 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 = data_segments + .iter() + .map(|(off, d)| synth_core::static_data_addr::DataSegment { + linmem_off: *off, + bytes: d.clone(), + }) + .collect(); + let data_rom_image: Vec = + 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::>() + .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). // diff --git a/crates/synth-cli/tests/vcr_ver_003_addr_777.rs b/crates/synth-cli/tests/vcr_ver_003_addr_777.rs index f2d698d2..037db8f2 100644 --- a/crates/synth-cli/tests/vcr_ver_003_addr_777.rs +++ b/crates/synth-cli/tests/vcr_ver_003_addr_777.rs @@ -82,3 +82,207 @@ fn gale_overlapping_segments_compile_clean() { assert!(out.exists(), "expected a relocatable .o output"); let _ = std::fs::remove_file(&out); } + +// --------------------------------------------------------------------------- +// Phase 2 (#777 follow-ups): span class, self-contained ROM image, RV32. +// --------------------------------------------------------------------------- + +/// Write an inline wat to a temp file and return its path. +fn wat_file(name: &str, wat: &str) -> PathBuf { + let dir = std::env::temp_dir().join("synth_vcr_ver_003_ph2"); + std::fs::create_dir_all(&dir).expect("mkdir"); + let p = dir.join(name); + std::fs::write(&p, wat).expect("write wat"); + p +} + +fn compile(input: &std::path::Path, out_name: &str, extra: &[&str]) -> std::process::Output { + let out = std::env::temp_dir() + .join("synth_vcr_ver_003_ph2") + .join(out_name); + let mut args = vec![ + "compile", + input.to_str().unwrap(), + "--all-exports", + "-o", + out.to_str().unwrap(), + ]; + args.extend_from_slice(extra); + Command::new(synth()) + .args(&args) + .output() + .expect("run synth") +} + +/// The span-class fixture: a STAGGERED overlap (seg_1 overwrites only seg_0's +/// tail) with an i32 load whose ADDEND byte is runtime-correct (owned by +/// seg_0) but whose 4-byte span crosses into seg_1's runtime-owned bytes — +/// the packed `__synth_wasm_seg_0` blob serves stale `a4 a5` where the +/// runtime image holds `b0 b1`. Phase 1 (addend byte only) accepted this and +/// emitted the miscompile (verified by hand on the v0.46 binary: compiles +/// clean, `.data` = seg_0's bytes verbatim). The load at 65542 straddles +/// 65544 where seg_1 takes over. +const SPAN_STRADDLE_WAT: &str = r#"(module + (memory (export "memory") 2) + (global $sp (mut i32) (i32.const 65536)) + (data (i32.const 65540) "\a0\a1\a2\a3\a4\a5\a6\a7") + (data (i32.const 65544) "\b0\b1\b2\b3") + (func (export "read_straddle") (result i32) + i32.const 65542 + i32.load))"#; + +/// PHASE-2 RED (span class): the straddling access is a genuine miscompile no +/// per-segment packing can serve (its bytes live in two non-adjacent packed +/// blobs), so the compile must FAIL LOUDLY with the span diagnostic — phase 1 +/// shipped it silently. +#[test] +fn span_straddling_overlap_is_refused_on_the_mixed_split() { + let fixture = wat_file("span_straddle_777.wat", SPAN_STRADDLE_WAT); + let out = compile( + &fixture, + "span_straddle_777.o", + &[ + "--target", + "cortex-m3", + "--native-pointer-abi", + "--relocatable", + ], + ); + let stderr = String::from_utf8_lossy(&out.stderr); + assert!( + !out.status.success(), + "the straddling stale-tail access MUST be refused (phase 1 silently \ + miscompiled it — the packed seg_0 serves a4a5 where the runtime \ + image owns b0b1):\nstderr: {stderr}" + ); + assert!( + stderr.contains("VCR-VER-003") && stderr.contains("span byte +2"), + "the refusal must carry the span diagnostic:\n{stderr}" + ); +} + +/// GREEN companion (same overlapping segments, non-straddling access): the +/// load at 65544 is owned by seg_1 and its span stays inside seg_1 + the +/// uncovered implicit-zero tail — the mixed split serves it correctly and the +/// module must keep compiling clean (the span check must not blanket-refuse +/// overlap shapes). +#[test] +fn span_owner_access_on_same_overlap_compiles_clean() { + let wat = r#"(module + (memory (export "memory") 2) + (global $sp (mut i32) (i32.const 65536)) + (data (i32.const 65540) "\a0\a1\a2\a3\a4\a5\a6\a7") + (data (i32.const 65544) "\b0\b1\b2\b3") + (func (export "read_owner") (result i32) + i32.const 65544 + i32.load))"#; + let fixture = wat_file("span_owner_777.wat", wat); + let out = compile( + &fixture, + "span_owner_777.o", + &[ + "--target", + "cortex-m3", + "--native-pointer-abi", + "--relocatable", + ], + ); + let stderr = String::from_utf8_lossy(&out.stderr); + assert!( + out.status.success(), + "the correctly-owned access must compile clean:\n{stderr}" + ); + assert!( + !stderr.contains("VCR-VER-003"), + "VCR-VER-003 must stay silent on the servable access:\n{stderr}" + ); +} + +/// Self-contained twin (#758 ROM-copy class): the SAME straddling module is +/// correct on the self-contained path — the dense flash image (index = linmem +/// offset, later-wins fill) preserves adjacency and overlap, so the straddle +/// reads `a2 a3 b0 b1` exactly as WASM semantics demand. It must compile +/// clean with the (unconditional) dense-image validator silent. The red side +/// of this class is the permanent `rom_image_red_on_first_wins_green_on_last_wins` +/// unit gate in synth_core::static_data_addr (the overwrite policy is an +/// argument — phase 1's `resolve_owner` pattern). +#[test] +fn span_straddle_module_selfcontained_rom_image_validates() { + let fixture = wat_file("span_straddle_777_sc.wat", SPAN_STRADDLE_WAT); + let out = compile( + &fixture, + "span_straddle_777_sc.elf", + &["--target", "cortex-m3"], + ); + // tracing goes to stdout; hard errors to stderr — scan both. + let all = format!( + "{}{}", + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ); + assert!( + out.status.success(), + "the dense self-contained image serves the straddle correctly — must \ + compile clean:\n{all}" + ); + assert!( + !all.contains("VCR-VER-003"), + "the dense-image validator must be silent on the correct pack:\n{all}" + ); + // The #758 ROM image must actually be present (the validator ran on it). + assert!( + all.contains("#758 data ROM image"), + "expected the #758 ROM-copy layout on this module:\n{all}" + ); +} + +/// RV32 class: the single-base scheme (s11, zeroed RAM) ships NO initializer +/// image, so a module with NONZERO active data is a silent-drop risk — the +/// (unconditional) zero-served-image validator must WARN LOUDLY. It is a +/// warning, not a hard error: the CI-pinned RV32 frozen fixture +/// (control_step.wasm) freezes compile-success on this path; the hard decline +/// + initializer shipping is the named follow-up. +#[test] +fn rv32_nonzero_data_segment_warns_loudly() { + let wat = r#"(module + (memory 1) + (data (i32.const 16) "\01\02\03\04") + (func (export "get") (result i32) i32.const 16 i32.load))"#; + let fixture = wat_file("rv32_data_777.wat", wat); + let out = compile(&fixture, "rv32_data_777.o", &["-b", "riscv"]); + // The warn! goes to stdout (tracing's default writer); scan both streams. + let all = format!( + "{}{}", + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ); + assert!(out.status.success(), "RV32 compile stays green:\n{all}"); + assert!( + all.contains("VCR-VER-003") && all.contains("read as 0x00"), + "nonzero dropped initializers must warn loudly:\n{all}" + ); +} + +/// RV32 non-vacuity: an all-zero runtime image (here a nonzero segment +/// OVERWRITTEN to zero by a later one — later-wins, not a bytes-grep) IS +/// served correctly by zeroed RAM, so the validator must stay silent. +#[test] +fn rv32_zero_overwritten_data_stays_silent() { + let wat = r#"(module + (memory 1) + (data (i32.const 16) "\01\02\03\04") + (data (i32.const 16) "\00\00\00\00") + (func (export "get") (result i32) i32.const 16 i32.load))"#; + let fixture = wat_file("rv32_zero_777.wat", wat); + let out = compile(&fixture, "rv32_zero_777.o", &["-b", "riscv"]); + let all = format!( + "{}{}", + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ); + assert!(out.status.success(), "RV32 compile stays green:\n{all}"); + assert!( + !all.contains("VCR-VER-003"), + "zeroed RAM serves the all-zero runtime image — no warning:\n{all}" + ); +} From 1211a6160c6ac0d1590af8b3c7df5662d599efba Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 06:39:40 +0200 Subject: [PATCH 3/5] =?UTF-8?q?docs(#777-ph2):=20VCR-VER-003=20phase-2=20s?= =?UTF-8?q?cope=20notes=20=E2=80=94=20roadmap=20+=20claims=20pins?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Roadmap: phase-2 landed items (5)-(8) — spanned reloc check w/ documented uncovered-byte residue, #758 dense ROM-image validation, RV32 zero-served warning (hard decline held on the frozen fixture, named follow-up), AArch64 verified N/A; steps + pass-criteria extended. claims.yaml: count-eq pins hold the phase-2 wiring unconditional (1 spanned call, 2 served-image calls in main.rs). claim_check 21/21 green. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/verified-codegen-roadmap.yaml | 64 ++++++++++++++++++++++--- claims.yaml | 22 +++++++++ 2 files changed, 80 insertions(+), 6 deletions(-) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index f296b1ea..57dd3042 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/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 diff --git a/claims.yaml b/claims.yaml index 0f3f36d9..4fa1fd16 100644 --- a/claims.yaml +++ b/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 From 26219f38577e2dae6d9f6438db160deb46daedbe Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 06:40:24 +0200 Subject: [PATCH 4/5] =?UTF-8?q?docs(#777-ph2):=20CLAUDE.md=20Track=20C=20?= =?UTF-8?q?=E2=80=94=20VCR-VER-003=20phase-2=20coverage=20note?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CLAUDE.md | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index 99fe1892..a0b580e5 100644 --- a/CLAUDE.md +++ b/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 From 8530a3c2c031a5c60c53ac5467f0ee1d054519c1 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 06:44:00 +0200 Subject: [PATCH 5/5] fix(#777-ph2): pin the shipped blob at the addend byte too (span byte 0) The spanned loop started at j=1, so a blob-fill divergence at exactly the addend byte (segment bytes green, shipped blob wrong) was unchecked while the rustdoc claimed otherwise. Check j=0 against the blob, deduped against the phase-1 segment-byte report; red-first unit gate span_red_on_blob_fill_corruption_at_addend_byte. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-core/src/static_data_addr.rs | 46 ++++++++++++++++++++++- 1 file changed, 44 insertions(+), 2 deletions(-) diff --git a/crates/synth-core/src/static_data_addr.rs b/crates/synth-core/src/static_data_addr.rs index 60dd6076..d294dabc 100644 --- a/crates/synth-core/src/static_data_addr.rs +++ b/crates/synth-core/src/static_data_addr.rs @@ -338,12 +338,22 @@ pub fn validate_reloc_resolutions_spanned( let Some(&poff) = packed.seg_packed_off.get(r.seg_index) else { continue; // impossible when layout and segments are parallel }; - for j in 1..MAX_ACCESS_BYTES { + for j in 0..MAX_ACCESS_BYTES { let access_addr = seg.linmem_off.wrapping_add(r.addend).wrapping_add(j); - // Unknown-width tolerance: runtime-uncovered ⇒ implicit zero ⇒ skip. + // Unknown-width tolerance: runtime-uncovered ⇒ implicit zero ⇒ skip + // (for j = 0 a missing runtime byte was already flagged by the + // strict phase-1 pass above). let Some(&runtime_byte) = runtime.get(&access_addr) else { continue; }; + // j = 0: the phase-1 pass already reported a divergent SEGMENT + // byte; re-checking here would double-report it. Only the blob + // side remains to pin — fall through when the segment byte is + // phase-1-green so a blob-fill bug (blob ≠ seg[K].bytes at the + // addend byte) still fails. + if j == 0 && seg.bytes.get(r.addend as usize) != Some(&runtime_byte) { + continue; + } let p = poff as usize + r.addend as usize + j as usize; // Served byte: the emitted blob, or "not linear memory at all" // when the span escapes the init region (globals slots / past the @@ -821,6 +831,38 @@ mod tests { } } + /// The blob-fill pin at the addend byte: segments and resolution are + /// phase-1-green, but the SHIPPED blob was corrupted at the served + /// position — the spanned validator must flag it at span byte 0 (phase 1 + /// reads segment bytes and cannot see it). + #[test] + fn span_red_on_blob_fill_corruption_at_addend_byte() { + let segs = vec![DataSegment { + linmem_off: 0x100, + bytes: vec![1, 2, 3, 4], + }]; + let (offs, mut blob) = mixed_pack(&segs); + let r = resolve_owner(&segs, 0x102, true).unwrap(); + assert_eq!( + validate_reloc_resolutions(&segs, std::slice::from_ref(&r)), + Verdict::Consistent, + "phase 1 (segment bytes) cannot see a blob-fill bug" + ); + blob[2] = 0xEE; // corrupt the byte the reloc actually serves + let packed = PackedInit { + seg_packed_off: &offs, + bytes: &blob, + }; + match validate_reloc_resolutions_spanned(&segs, std::slice::from_ref(&r), &packed) { + Verdict::Mismatch(m) => { + assert_eq!(m[0].span_byte, 0); + assert_eq!(m[0].served, 0xEE); + assert_eq!(m[0].runtime, 3); + } + Verdict::Consistent => panic!("VACUOUS: corrupted shipped blob accepted"), + } + } + /// ROM-image RED-FIRST (self-contained class, phase 1's `resolve_owner` /// pattern — the overwrite policy is an ARGUMENT): on an overlapping /// module the SAME dense-image validator must be RED on the first-wins