From 34319b95364f2a55c8ba1bdadaad3d6ec18581f6 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 22 Jun 2026 18:01:06 +0200 Subject: [PATCH] test(vcr-mem): layer-2 end-to-end budget pipeline on real gust fixture (#242, #383) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the join the #392 spike and the shadow_budget unit suite each cover only half of: `layer2_budget_pipeline_msgq_end_to_end_383` (synth-cli main.rs cfg(test)) runs scry's `analyze()` on the REAL msgq_put_359.wasm gust fixture, maps its proven StackBound through the synth-owned StackDepthBound (the 1:1 adapter that becomes `impl From` when 2b promotes scry to a production dep), feeds `budget_from_bound`, and asserts the 2048x over-reservation (65536 B page) collapses to a PROVEN 32-byte budget — source=ProvenStackDepth, preferred over the asserted 4096 fallback. Frozen-safe: scry-sai-core stays a DEV-dependency exercised only under cfg(test), so the production binary pulls no scry and emits identical bytes (the change is entirely in #[cfg(test)] code). No MODULE.bazel pin (tests are not in the Bazel graph). Independent of the from_cargo migration (#422) — it uses the existing dev-dep under the current resolution. This test is the oracle the gated 2b wiring (`--shadow-stack-size auto`) must match. Roadmap VCR-MEM-001 updated with the end-to-end criterion. Verification: `cargo test -p synth-cli --bin synth layer2_budget_pipeline` → pass (alongside the 9 shadow_budget units); fmt + clippy -D warnings clean; rivet check zero non-xref errors. Co-Authored-By: Claude Opus 4.8 --- artifacts/verified-codegen-roadmap.yaml | 11 +++++ crates/synth-cli/src/main.rs | 61 +++++++++++++++++++++++++ 2 files changed, 72 insertions(+) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 18daeaad..16e44051 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -1183,6 +1183,17 @@ artifacts: passes with scry ABSENT from the build graph (dep-free synth-owned bound enum). The scry production-dep wiring (2a/2b above) is the separate gated step; default-off ⇒ frozen fixtures unaffected. + LAYER (2) END-TO-END criterion (LANDED 2026-06-22, frozen-safe): the + join the #392 spike (scry raw output only) and the decision-logic suite + (synthetic bounds only) each cover half of — `layer2_budget_pipeline_msgq + _end_to_end_383` (synth-cli main.rs cfg(test)) runs scry's `analyze()` on + the REAL msgq_put_359.wasm gust fixture, maps StackBound→StackDepthBound + (the 1:1 adapter that becomes `impl From` in 2b), feeds budget_from_bound, + and asserts the 2048x over-reservation (65536) collapses to a PROVEN 32 B + budget (source=ProvenStackDepth, preferred over the asserted 4096 + fallback). scry stays a DEV-dep exercised only under cfg(test) ⇒ the + production binary pulls no scry and emits identical bytes. This test is + the oracle the gated 2b wiring must match. - id: VCR-MEM-002 type: sw-req diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index f02153e7..8a0a27a8 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -4153,6 +4153,67 @@ mod tests { } } + /// VCR-MEM-001 layer-2 END-TO-END (#242, #383): prove the full budget + /// pipeline on the REAL gust-family fixture — scry's proven shadow-stack + /// depth, mapped through the synth-owned bound, yields the `budget_from_bound` + /// decision (the #421 logic) that the gated `--shadow-stack-size auto` wiring + /// will consume. This is the join the #392 spike (which stops at scry's raw + /// output) and the `shadow_budget` unit suite (which tests the decision on + /// synthetic bounds) each cover only half of. + /// + /// Frozen-safe: `scry-sai-core` is a DEV-dependency exercised only under + /// `cfg(test)`, so the production binary pulls no scry and emits no different + /// bytes — the frozen fixtures stay bit-identical by construction. When step + /// 2b promotes scry to a (feature-gated) production dep, the inline 1:1 + /// adapter below becomes an `impl From` and this test is the + /// oracle that the wiring matches. + #[test] + fn layer2_budget_pipeline_msgq_end_to_end_383() { + use scry_analyze_core::{AnalysisConfig, StackBound, analyze}; + use shadow_budget::{BudgetDecision, BudgetSource, StackDepthBound, budget_from_bound}; + + let fixture = std::path::Path::new(env!("CARGO_MANIFEST_DIR")) + .join("../../scripts/repro/msgq_put_359.wasm"); + let bytes = std::fs::read(&fixture).expect("the #359/#383 gust-family fixture is in-tree"); + + let r = analyze( + bytes, + AnalysisConfig { + widening_threshold: None, + emit_diagnostics: false, + taint_policy: None, + }, + ) + .expect("scry analyzes a valid Core module"); + + // Adapter: scry's StackBound -> synth's dep-free StackDepthBound (1:1; + // becomes a `From` impl when scry graduates to a production dep in 2b). + let bound = match r.stack_usage.max_stack_bytes { + StackBound::Bytes(n) => StackDepthBound::Bytes(n), + StackBound::Unbounded => StackDepthBound::Unbounded, + StackBound::Unknown => StackDepthBound::Unknown, + }; + + // msgq_put reserves the full declared page (sp_init = 65536 = the + // .bss [0,65536) stack span the roadmap recorded); scry proves the true + // worst case is 32 B. The derived budget is sp_init-independent for any + // sp_init above the depth — what matters is the PROVEN 32 vs the page. + let sp_init = 65_536; + let decision = budget_from_bound(bound, sp_init, Some(4096)); + + // End-to-end: a 2048x over-reservation collapses to a PROVEN 32-byte + // budget — and, with a fallback available, the proven path is preferred + // over the asserted one (source is ProvenStackDepth, not AssertedFallback). + assert_eq!( + decision, + BudgetDecision::Use { + bytes: 32, + source: BudgetSource::ProvenStackDepth + }, + "scry-proven 32 B depth -> proven 32 B budget, not the asserted 4096 fallback" + ); + } + /// #235: a dissolved export's non-exported callee must be pulled into the /// reachable set (so it lands in the relocatable object), while imports and /// unreachable functions stay out.