From 9b09a9321756232e559710b7930e514726bc532c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 22 Jun 2026 20:23:45 +0200 Subject: [PATCH] =?UTF-8?q?test(vcr-mem):=20layer-2=20honest-fail=20safety?= =?UTF-8?q?=20oracle=20=E2=80=94=20unbounded=20recursion=20refuses=20a=20p?= =?UTF-8?q?roven=20budget=20(#242,=20#383)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The msgq/gust tests cover layer-2's PROVEN (finite) path; the soundness of the whole derivation rests on the complementary REFUSAL path working — an unbounded shadow stack must never receive a finite budget, or the image silently under-reserves and overflows on silicon. #421 covers this with synthetic bounds only; this anchors it against REAL scry output. `scripts/repro/recursive_shadow_stack.wat` recurses through the shadow stack (each activation decrements the SP global by a 16 B frame), so the worst-case depth is unbounded. Empirically scry classifies it exactly: sp_global identified, recursive=true, max_stack_bytes=Unbounded. `layer2_unbounded_recursion_refuses_proven_budget_242` (synth-cli main.rs cfg(test)) asserts that scry behaviour AND that `budget_from_bound` never yields a ProvenStackDepth for it — with a fallback it returns AssertedFallback (not proven), without one it honestly refuses. This guards the upstream assumption the entire honest-fail gate depends on: a scry regression that returned a finite bound for an unbounded stack — the one failure mode that would silently under-reserve on silicon — would redden CI. Frozen-safe: scry + wat stay test-only (cfg(test)); production bytes unchanged, no MODULE.bazel pin. Roadmap VCR-MEM-001 records the proven+honest-fail coverage. Verification: `cargo test -p synth-cli --bin synth layer2_` -> 3/3 pass; fmt + clippy -D warnings clean; rivet check zero non-xref errors. Co-Authored-By: Claude Opus 4.8 --- artifacts/verified-codegen-roadmap.yaml | 13 ++++ crates/synth-cli/src/main.rs | 75 ++++++++++++++++++++++++ scripts/repro/recursive_shadow_stack.wat | 24 ++++++++ 3 files changed, 112 insertions(+) create mode 100644 scripts/repro/recursive_shadow_stack.wat diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index f974a5fe..e283d2ec 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -1204,6 +1204,19 @@ artifacts: 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. + LAYER (2) PROVEN-DEPTH + HONEST-FAIL coverage (LANDED 2026-06-22, + frozen-safe): the proven path is now anchored on BOTH real shadow-stack + fixtures — msgq (Bytes(32)) and gust_kernel (Bytes(16), the fixture jess + flashes; proven ≤ flashed 4096, silicon budget sound, #424). The + soundness-critical REFUSAL path is anchored against real scry output via + `recursive_shadow_stack.wat` (recurses through the SP global ⇒ scry + returns recursive=true + Unbounded): `layer2_unbounded_recursion_refuses + _proven_budget_242` asserts an unbounded depth NEVER yields a + ProvenStackDepth — only the asserted fallback (if given) or an honest + refuse. This guards the upstream assumption the entire honest-fail gate + rests on (scry flags recursion-through-the-shadow-stack as non-finite), so + a scry regression that returned a finite bound for an unbounded stack — + the one failure that would silently under-reserve on silicon — reddens CI. - id: VCR-MEM-002 type: sw-req diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index 164a28fe..a18a797f 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -4291,6 +4291,81 @@ mod tests { ); } + /// VCR-MEM-001 layer-2 HONEST-FAIL SAFETY ORACLE (#242, #383): the soundness + /// of the whole budget derivation rests on an upstream assumption — that scry + /// returns a NON-finite bound for a stack that can grow without bound, so the + /// derivation refuses rather than inventing a finite budget that would + /// silently under-reserve and overflow on silicon. The msgq/gust tests cover + /// the proven (finite) path; this covers the refusal path against REAL scry + /// output, guarding the assumption directly. + /// + /// `recursive_shadow_stack.wat` recurses through the shadow stack (each + /// activation decrements the SP global by a frame), so the depth is + /// unbounded. We assert scry detects that (recursive + Unbounded) AND that + /// `budget_from_bound` never yields a ProvenStackDepth for it — only the + /// asserted fallback (if given) or an honest refuse. + /// + /// Frozen-safe: scry + wat stay test-only here; production bytes unchanged. + #[test] + fn layer2_unbounded_recursion_refuses_proven_budget_242() { + use scry_analyze_core::{AnalysisConfig, StackBound, analyze}; + use shadow_budget::{BudgetDecision, BudgetSource, StackDepthBound, budget_from_bound}; + + let wat_path = std::path::Path::new(env!("CARGO_MANIFEST_DIR")) + .join("../../scripts/repro/recursive_shadow_stack.wat"); + let wasm = wat::parse_file(&wat_path).expect("the honest-fail fixture .wat parses"); + + let r = analyze( + wasm, + AnalysisConfig { + widening_threshold: None, + emit_diagnostics: false, + taint_policy: None, + }, + ) + .expect("scry analyzes the recursive Core module"); + + // The upstream assumption the honest-fail gate depends on: recursion + // through the shadow stack is detected and has NO finite bound. + assert!( + r.function_summaries.iter().any(|s| s.recursive), + "scry detects the shadow-stack recursion" + ); + assert_eq!( + r.stack_usage.max_stack_bytes, + StackBound::Unbounded, + "recursion through the shadow stack has no finite proven bound" + ); + + let bound = match r.stack_usage.max_stack_bytes { + StackBound::Bytes(n) => StackDepthBound::Bytes(n), + StackBound::Unbounded => StackDepthBound::Unbounded, + StackBound::Unknown => StackDepthBound::Unknown, + }; + + // SAFETY (1): with a fallback, the budget is the integrator-ASSERTED one — + // explicitly NOT ProvenStackDepth. An unbounded stack never gets a proven + // finite budget; the proof label is reserved for a real finite depth. + assert_eq!( + budget_from_bound(bound, 65_536, Some(4096)), + BudgetDecision::Use { + bytes: 4096, + source: BudgetSource::AssertedFallback + }, + "unbounded depth -> asserted fallback, never ProvenStackDepth" + ); + + // SAFETY (2): with no fallback, an honest refuse — never an invented + // number for a stack the analyzer could not bound. + match budget_from_bound(bound, 65_536, None) { + BudgetDecision::Refuse(msg) => assert!( + msg.contains("unbounded"), + "refusal names the unbounded cause; got: {msg}" + ), + other => panic!("unbounded + no fallback must refuse, got {other:?}"), + } + } + /// #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. diff --git a/scripts/repro/recursive_shadow_stack.wat b/scripts/repro/recursive_shadow_stack.wat new file mode 100644 index 00000000..c4ccd897 --- /dev/null +++ b/scripts/repro/recursive_shadow_stack.wat @@ -0,0 +1,24 @@ +;; VCR-MEM-001 layer-2 honest-fail fixture (#242, #383). +;; +;; A function that recurses THROUGH the shadow stack: each activation decrements +;; the stack-pointer global by a 16-byte frame before calling itself, so the +;; worst-case shadow-stack depth grows without bound. This is the case the +;; layer-2 budget derivation MUST refuse — deriving any finite budget for an +;; unbounded stack would silently under-reserve and overflow on silicon. +;; +;; scry classifies this exactly: sp_global identified, function recursive, +;; max_stack_bytes = Unbounded. The test +;; `layer2_unbounded_recursion_refuses_proven_budget_242` asserts that scry +;; behaviour AND that `budget_from_bound` never returns a ProvenStackDepth for +;; it — only the asserted fallback (if given) or an honest refuse. +(module + (global $sp (mut i32) (i32.const 65536)) + (memory 1) + (func $recurse (param $n i32) + ;; allocate a 16-byte shadow-stack frame + (global.set $sp (i32.sub (global.get $sp) (i32.const 16))) + (if (local.get $n) + (then (call $recurse (i32.sub (local.get $n) (i32.const 1))))) + ;; free the frame + (global.set $sp (i32.add (global.get $sp) (i32.const 16)))) + (func (export "run") (call $recurse (i32.const 10))))