test(vcr-mem): layer-2 honest-fail safety oracle — unbounded recursion refuses a proven budget (#242, #383) (#425)

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 <noreply@anthropic.com>

Author: avrabe

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

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.

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))))