feat(vcr-mem): layer-2 shadow-stack budget decision logic, frozen-safe (#242, #383)

[avrabe]

What

VCR-MEM-001 layer-2 derives the shadow-stack budget B from a proven worst-case stack depth instead of the integrator-asserted number that layer-1 (#383, v0.11.51) trusts. This PR lands the decision logic only — the dep-free core — ahead of the gated scry-production-dep wiring.

crates/synth-cli/src/shadow_budget.rs: a pure

budget_from_bound(bound: StackDepthBound, sp_init: u32, fallback: Option<u32>) -> BudgetDecision

over a synth-owned StackDepthBound enum (Bytes(u64) | Unbounded | Unknown). Because the enum is synth's own (not scry_analyze_core::StackBound), the logic and its 9 unit tests compile and run with scry absent from the build graph — and, critically, without scry's ~28-crate transitive closure entering the Bazel rust_binary compile. The adapter from scry's type lives at the future (gated) call site.

Soundness scope — "proven stack DEPTH, asserted no-heap"

Confirmed against the primary source (scry-sai-core-1.12 lib.rs:276-281): max_stack_bytes is "the deepest weighted path through the call graph, each function weighted by the frame its prologue subtracts from the __stack_pointer global … guest shadow-stack only." That is exactly the [0, sp_init) region B controls.

• Bytes(n) → source = ProvenStackDepth, B = align16(n) — labelled "proven stack depth, asserted no-heap". Never restated as a bare "proven footprint" (the native-pointer-abi: size the wasm .bss to data high-water-mark, not the full declared memory page (blocks tiny-RAM targets) #383 overclaim shape is explicitly guarded).
• Bytes(n) with n > sp_init → refuse, naming it as the original image under-provisioning its stack (a latent source bug surfaced for free, not a generic refuse).
• Unbounded / Unknown → AssertedFallback if a fallback is given, else honest refuse with the cause. Unknown never yields ProvenStackDepth, even with a fallback (unit-tested).
• B rounded up to 16-byte AAPCS/LLVM stack alignment — rounding up preserves B ≥ proven depth, so soundness is not weakened.

Frozen-safe

No call site yet (#[allow(dead_code)]), no byte-changing codegen, default behaviour unchanged. Frozen fixtures (control_step 0x00210A55, flat+inlined flight_algo 0x07FDF307, divseam) are untouched by construction.

Remaining gated steps (recorded in the roadmap)

• 2a — dep architecture (user decision): promoting scry-sai-core dev-dep → production dep pulls its closure into the Bazel graph (synth-cli is built there, crates/BUILD.bazel:230; MODULE.bazel uses crate.from_specs(), likely because z3 needs static-link-z3). Choice among {from_cargo migration, feature-gate the scry call out of the Bazel build, ~28 manual specs} — not a unilateral call.
• 2b — adapter + wiring: scry::StackBound → StackDepthBound adapter at a call site running analyze(), routed into the layer-1 shrink; opt-in (--shadow-stack-size auto); verifies-link scry SCRY-001.

Verification

• cargo test -p synth-cli --bin synth shadow_budget → 9/9 pass
• cargo fmt --check clean; cargo clippy -p synth-cli --all-targets -- -D warnings clean
• rivet check → zero non-xref errors

Refs #242 (VCR epic), #383 (layer-1).

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 96.25000% with 3 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-cli/src/shadow_budget.rs	96.25%	3 Missing ⚠️

📢 Thoughts on this report? Let us know!