test(vcr-mem): layer-2 honest-fail safety oracle — unbounded recursion refuses a proven budget (#242, #383)#425
Merged
Conversation
…n refuses a proven budget (#242, #383) 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>
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Jun 22, 2026
, #394) (#440) First release of the north-star verified-codegen campaign. Pin sweep 0.11.51 -> 0.12.0 (workspace + all path-dep versions + MODULE.bazel + Cargo.lock), CHANGELOG, and VCR-DBG-001 roadmap status -> implemented. Ships: - VCR-DBG-001 `--debug-line` DWARF emission (PR A #427 / B #429 / C #430): debugger-readable .debug_* mapping ARM .text -> wasm source lines, with .rel.debug_* relocations verified end-to-end against arm-none-eabi-ld. Purely additive; default build bit-identical. - VCR-MEM-001 layer-2 frozen-safe budget decision logic + oracles (#421-#425). - gimli 0.33 adaptation (#439) + wast 252 (#438). Minor bump: new user-facing `--debug-line` feature (semver-correct). Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
The msgq (#423) and gust_kernel (#424) tests cover layer-2's proven (finite) budget path. The soundness of the whole derivation equally depends on the refusal path: 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.watrecurses 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:layer2_unbounded_recursion_refuses_proven_budget_242asserts that scry behaviour and thatbudget_from_boundnever yields aProvenStackDepthfor it:AssertedFallback(explicitly not proven)Refuse, never an invented numberWhy it matters (not corpus-fill)
This guards the upstream assumption the entire honest-fail gate rests on — that scry flags recursion-through-the-shadow-stack as non-finite. The one failure mode that would make layer-2 unsafe is scry returning a finite bound for an unbounded stack (→ silent under-reservation on silicon). If a future scry bump regressed that, this test reddens CI. It's the safety complement to the two proven-path tests.
Frozen-safe
scry +
watstay test-only (cfg(test)); production bytes unchanged, no MODULE.bazel pin. Roadmap VCR-MEM-001 records the combined proven + honest-fail coverage.Verification
cargo test -p synth-cli --bin synth layer2_→ 3/3 pass (msgq proven, gust proven, recursion refused)cargo fmt --checkclean;cargo clippy -p synth-cli --all-targets -- -D warningscleanrivet check→ zero non-xref errorsRefs #242, #383.
🤖 Generated with Claude Code