diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 8017588a..2ab5a5d4 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -842,3 +842,114 @@ artifacts: (v0.11.40 gate) the release notes report the measured cycle-gap delta attributable to scry-driven remat + narrowing, feeding VCR-DEC-001's revisit decision. + + - id: VCR-MEM-001 + type: sw-req + title: "Bounded + provable native-pointer linear-memory footprint (shadow-stack budget → scry stack-depth AI) — gale #383" + description: > + gale #383: under --native-pointer-abi, build_relocatable_elf + (synth-cli/src/main.rs:2475) sizes the wasm linmem region to + used_extent = max(data_end, sp_top, global_top, static_top, + static_top_abs32).min(linear_memory_bytes). The sp_top term is sp_init — + the shadow-stack top, which wasm-ld sets to the DECLARED page top (65536 + for `(memory 1)`). So the region spans [0, 65536) even when actual data + + live stack is a few KB, and an 8 KiB-RAM target (STM32F100) cannot place + it. MEASURED 2026-06-20 (synthetic repro, no gale binary needed — + reproduced like #354/#382): a `(memory 1)` module with sp_init=65536 + emits a 64 KiB NOBITS .bss (all-zero linmem) or a 64 KiB PROGBITS .data + (with an init segment below the static region). Root cause is purely + structural — sp_top dominates used_extent. + + DO NOT fix as a bare CLI cap (integrator declares a number, synth shrinks + the reservation blindly): shrinking below the live shadow-stack depth + silently overflows the stack into static data. The integrator declaring a + RAM budget is the INPUT; the obligation is to keep the footprint claim + HONEST about what is proven vs asserted. CRITICAL DISCOVERY (2026-06-20): + synth has ZERO shadow-stack tracking today — the comment at main.rs:2522 + ("the shadow stack is reached only via the SP register value, dynamic, + never a static reloc") confirms it treats [0, sp_init) as opaque. So the + shadow stack is a wasm-level construct (the __stack_pointer global's + decrement idiom), NOT the ARM machine-stack frame_size. Computing its + depth is a NEW abstract interpretation — which is scry's mandate. Layered + by risk (advisor-reviewed) so the unblock does NOT depend on the new AI: + + (1) LOAD-BEARING — layout re-base + integrator budget + consistency + check + honest refuse (THIS issue's fix). New + `--shadow-stack-size ` on `compile`: re-base sp_init to a + budget B instead of the declared page top. Output is "asserted + (B), not proven"; DEFAULT unset = full-page = byte-identical + (frozen-safe). SCOPE CORRECTION (2026-06-20, measured on the REAL + gust-family module msgq_put_359.wasm, not just a synthetic repro): + sp_init doubles as the selector's classification boundary + (set_native_pointer_stack → wasm_data_base, instruction_selector.rs:1623; + classify at 6735/6846: addr >= boundary ⇒ static `__synth_wasm_data + C` + reloc, < ⇒ SP-relative frame). The selector ALREADY RAN with + boundary=65536, so a pure post-selection re-base is sound ONLY when + nothing was classified against it (no static reloc). BUT the real + msgq module carries 10 `__synth_wasm_data` relocs (zero-init + k_spinlock-class statics ABOVE the shadow stack: .bss=0x10018=65560 = + stack [0,65536) + zero statics [65536,65560)). So pure-only REFUSES + on the real module — it would ship green and NOT unblock gale. The + actual layer-1 is the #354 per-region retarget extended to the + NOBITS region: shift the high `__synth_wasm_data + C` (C >= boundary) + relocs DOWN by (sp_init - B) and size the .bss to B + zero-static + extent, so the stack reservation shrinks while the zero statics + stay covered. Re-bases the SP global slot init to B. Sound (stack + grows down from B; statics at [B, B+ext) above it never overlap). + HONEST REFUSE for unhandled geometries (static C below the stack / + B > sp_init / non-Abs32 static relocs). This is link-fragile + native-pointer surgery (the #354 step-2 work it explicitly + deferred) on the path gale FLIES ⇒ silicon-gated (held for gale + confirmation, the #368→#359 lesson — do not rush-ship). The one + open disambiguation posted to gale: does the gust target use the + --stack-first layout (statics above the stack, as msgq shows) so + the down-shift is a uniform addend rewrite. + (2) OPT-IN, NOT LOAD-BEARING — conservative auto-proof: where the + reachable graph is ACYCLIC + direct-call-only + every reachable + function matches the canonical single-`sub`-at-entry shadow-frame + idiom, synth PROVES max_depth = longest weighted path over the + reachable DAG (reachable_from_exports, main.rs:1671), weight = the + per-function __stack_pointer decrement held ACROSS calls (not merely + the entry decrement; multiple/conditional/variable SP adjustments or + SP-stored-elsewhere ⇒ REFUSE). This upgrades (1)'s "asserted" to + "proven" with no integrator input; on refuse it falls back to (1). + call_indirect MUST force refuse — reachable_from_exports + over-approximates indirect by pulling in ALL table funcs (sound for + reachability, but for longest-path the edge set explodes and can + fabricate cycles). DISCRIMINATING RISK (advisor): kernels usually + dispatch through tables, so if gale's gust kernel uses call_indirect + this auto-proof refuses and ONLY (1) unblocks it — do not bet the + unblock on (2). (This is the #383 ↔ #275 link.) + (3) SCRY TAIL (VCR-RA-010 / SCRY-001, scry#51): scry proves the + indirect/recursive tail (call_indirect target sets, recursion + bounds, reachability narrowing) that (2) refuses — the sound + abstract interpretation synth cannot do alone. + Build order: (1) now (this release), (2) immediately after, (3) as scry#51 + matures. The proven-minimal path stays opt-in until silicon-validated (the + native-pointer #345/#354/#359 lesson — gale/jess confirms the final image). + status: proposed + tags: [codegen, native-pointer-abi, memory-layout, abstract-interpretation, scry, stack-depth, gale-383, track-a] + links: + - type: derives-from + target: VCR-001 + - type: traces-to + target: VCR-RA-010 + fields: + req-type: functional + priority: should + verification-criteria: > + LAYER (1), this release: with `--shadow-stack-size B`, a `(memory 1)` + native-pointer module (sp_init=65536, small static-data extent) reserves + static_data_high_water + B and re-bases sp_init to that top — a region + of a few KB instead of 64 KiB, placeable in an 8 KiB-RAM linker script. + Synth REFUSES honestly (typed Err, never silent shrink) when the + static-data high-water would collide with the re-based stack top. The + emitted footprint is labelled "asserted (B), not proven". WITHOUT the + flag the reservation and every byte are UNCHANGED ⇒ all frozen fixtures + (control_step 0x00210A55, flat+inlined flight_algo 0x07FDF307, divseam) + byte-identical. A post-link oracle asserts (a) stack region and data + region do not overlap AND (b) the reservation still covers every + relocated __synth_wasm_data access (the #359 msgq regression check). + LAYER (2), next: acyclic + direct-only + canonical-frame modules derive + B automatically (output "proven"); call_indirect / recursion / non-canonical + frame ⇒ refuse → fall back to (1). LAYER (3): scry#51 proves the tail. diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index 190325c5..1064816a 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -226,6 +226,22 @@ enum Commands { /// `docs/sigil-integration.md`. #[arg(long)] sign_output: bool, + + /// #383 (VCR-MEM-001): integrator-declared shadow-stack budget in BYTES + /// for the `--native-pointer-abi` linear-memory reservation. Without + /// this flag synth reserves the wasm linmem region up to the declared + /// page top (the SP global's init, e.g. 65536 for `(memory 1)`), which + /// is RAM-prohibitive on small MCUs. With it, the region is reserved as + /// `static_data_high_water + budget` and the shadow-stack top is + /// re-based to that smaller extent — so a few-KB-live module links into + /// an 8 KiB-RAM part. Synth REFUSES (does not silently shrink) if the + /// static-data high-water would collide with the re-based stack top. + /// The footprint is ASSERTED (the budget is trusted), not proven — + /// synth does not yet prove the program's max shadow-stack depth fits + /// the budget (that is the layer-2 auto-proof / scry tail, VCR-MEM-001). + /// Only meaningful with `--native-pointer-abi`. + #[arg(long, value_name = "BYTES")] + shadow_stack_size: Option, }, /// Disassemble an ARM ELF file (e.g., synth disasm output.elf) @@ -342,6 +358,7 @@ fn main() -> Result<()> { native_pointer_abi, sbom, sign_output, + shadow_stack_size, } => { // Resolve target spec: --target overrides, --cortex-m is backwards compat let target_spec = resolve_target_spec(target.as_deref(), cortex_m, &backend)?; @@ -381,6 +398,7 @@ fn main() -> Result<()> { native_pointer_abi, sbom_path, sign_output, + shadow_stack_size, )?; // If --link requested, invoke the cross-linker @@ -930,6 +948,7 @@ fn compile_command( native_pointer_abi: bool, sbom_path: Option, sign_output: bool, + shadow_stack_size: Option, ) -> Result<()> { // Validate backend exists let registry = build_backend_registry(); @@ -976,6 +995,7 @@ fn compile_command( native_pointer_abi, sbom_path, sign_output, + shadow_stack_size, ); } @@ -1730,6 +1750,7 @@ fn compile_all_exports( native_pointer_abi: bool, sbom_path: Option, sign_output: bool, + shadow_stack_size: Option, ) -> Result<()> { let path = input.context("--all-exports requires an input file")?; @@ -2176,6 +2197,7 @@ fn compile_all_exports( Some(NativeGlobalsLayout { globals: all_globals.clone(), sp_init: stack_pointer_global_opt.map(|(_, v)| v).unwrap_or(0), + shadow_stack_size, }) } else { None @@ -2320,6 +2342,13 @@ struct NativeGlobalsLayout { globals: Vec<(u32, i32)>, /// The shadow-stack top (the SP global's init); the region must cover it. sp_init: i32, + /// #383 (VCR-MEM-001): integrator-declared shadow-stack budget in bytes. When + /// `Some(B)`, the caller asked to shrink the [0, sp_init) reservation to `B` + /// (re-basing the stack top and shifting the high zero-init static relocs + /// down). The retarget surgery is silicon-gated (link-fragile native-pointer + /// path, the #368→#359 lesson); until it lands, a `Some` here is an honest + /// Err, never a silent no-op. + shadow_stack_size: Option, } fn build_relocatable_elf( @@ -2331,6 +2360,23 @@ fn build_relocatable_elf( ) -> Result> { use std::collections::HashMap; + // #383 (VCR-MEM-001): the integrator-declared shadow-stack budget shrinks the + // [0, sp_init) reservation by re-basing the stack top and shifting the high + // zero-init static relocs down. That is link-fragile native-pointer surgery on + // the path gale flies, so it is silicon-gated and not yet active. Fail HONESTLY + // (the #378/#381 contract) rather than accept the flag and silently ignore it. + if let Some(layout) = native_globals.as_ref() + && layout.shadow_stack_size.is_some() + { + anyhow::bail!( + "--shadow-stack-size is accepted but not yet active: the + native-pointer linear-memory shrink (re-base sp_init + retarget the + high zero-init static relocations down) is link-fragile and held for + on-silicon confirmation. Tracked as VCR-MEM-001 / gale #383. Omit the + flag to reserve the full declared page (current behaviour)." + ); + } + let mut elf_builder = ElfBuilder::new_arm32() .with_entry(0) .with_type(ElfType::Rel); // ET_REL: relocatable object @@ -4101,6 +4147,7 @@ mod tests { let native = NativeGlobalsLayout { globals: vec![(0, 65_536)], sp_init: 65_536, + shadow_stack_size: None, }; let elf = build_relocatable_elf(&[func], &[], &[], linear_memory_bytes, Some(native)) @@ -4195,6 +4242,7 @@ mod tests { let native = NativeGlobalsLayout { globals: vec![(0, 65_536)], sp_init: 65_536, + shadow_stack_size: None, }; let elf = build_relocatable_elf(&[func], &[], &[], 131_072, Some(native)) .expect("#345: native-pointer literal-pool object builds"); @@ -4275,6 +4323,7 @@ mod tests { let native = NativeGlobalsLayout { globals: vec![(0, 65_536)], sp_init: 65_536, + shadow_stack_size: None, }; let elf = build_relocatable_elf(&[func], &[], &data_segments, 131_072, Some(native))