test(vcr-mem): layer-2 cross-check on gust_kernel's flashed silicon budget (#242, #383)

[avrabe]

What

jess is flashing gust_kernel.wasm with an integrator-asserted --shadow-stack-size 4096 on the Renode-M3 / STM32F100 rung (gale#65). This adds the layer-2 cross-check on that live budget:

• scry proves gust_kernel's worst-case shadow-stack depth is Bytes(16) (sp_global=0, no recursion, 6 reachable).
• Proven 16 ≤ flashed 4096 → the asserted budget is sound, with a 256× margin — not an under-reservation.
• budget_from_bound(Bytes(16), sp_init=1048576, Some(4096)) → Use{16, ProvenStackDepth}: layer-2 would accept jess's budget and could auto-derive an even tighter 16 B (256× under 4096, 65536× under the 1 MiB declared-page default).

Previously only the asserted 4096 was on record; gust_kernel's proven depth was unmeasured. This is the safety sanity-check on the exact number going onto hardware.

Why it's not corpus-fill

layer2_gust_kernel_proven_depth_clears_flashed_budget_383 asserts proven ≤ flashed on the fixture jess actually flies. If a future scry bump ever raised gust_kernel's proven depth above the flashed budget, CI reddens before silicon, not after. It extends the msgq end-to-end pattern (#423) to the live-work fixture.

Frozen-safe

scry stays a dev-dep under cfg(test) → production bytes unchanged. No MODULE.bazel pin, no codegen change. Roadmap VCR-MEM-001 records the proven-vs-asserted finding.

Verification

• cargo test -p synth-cli --bin synth layer2_ → 2/2 pass (msgq + gust_kernel)
• cargo fmt --check clean; cargo clippy -p synth-cli --all-targets -- -D warnings clean
• rivet check → zero non-xref errors

Refs #242, #383 (gale#65 silicon rung).

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 96.15385% with 1 line in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-cli/src/main.rs	96.15%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!