Skip to content

rvm: add debug-mode invariant assertions - #59

Open
anakrish wants to merge 1 commit into
upstream-main-snapshotfrom
storage-abstraction-vm-invariants
Open

rvm: add debug-mode invariant assertions#59
anakrish wants to merge 1 commit into
upstream-main-snapshotfrom
storage-abstraction-vm-invariants

Conversation

@anakrish

@anakrish anakrish commented Jun 2, 2026

Copy link
Copy Markdown
Owner

Encode the RVM's stack, context, and register lifecycle invariants as debug_assert!s so future modifications can't quietly violate them. Zero cost in release; surfaces violations during the existing 600+ test suite in debug mode.

Motivation. The recent code-review pass on #58 raised 10 "state corruption on error path" findings against comprehension.rs / loops.rs. All 10 sat on terminal VmError paths that reset_execution_state wipes before reuse, so they were unobservable — but that was knowledge in our heads, not anything the test suite enforces. This PR pins the invariants down so the next person changing the RVM gets a loud failure instead of a silent leak.

What's asserted (all debug_assert!, all #[cfg(debug_assertions)]):

  • state.rs::debug_assert_state_is_clean() — post-condition of reset_execution_state: all stacks empty, registers resized to base_register_count and Undefined, rule_cache reset, pc == 0, builtins_cache empty, state Ready.
  • state.rs::assert_vm_invariants() — invoked per opcode at the top of run_stackless_loop and jump_to: state ∈ {Ready, Running}, registers non-empty, rule_cache sized to program, execution stack bounded.
  • execution.rs::resume — pre-condition: ExecutionState::Suspended { .. }.
  • execution.rs::execute_suspendable_entry — pre-condition: clean state.
  • Push/pop balance checks on comprehension_stack (comprehension.rs) and call_rule_stack (rules.rs), with a rule_index equality check on the run-to-completion finalize.
  • IterationState::advance (context.rs) — Single not double-consumed, Array index doesn't overflow.

Considered but rejected (documented in commit message): register_stack.len() == call_rule_stack.len() (suspendable mode stashes registers elsewhere); state == Running inside dispatch (entry-point dispatch legitimately runs in Ready); registers.len() >= base_register_count (rule frames swap in smaller private windows); frame-paired stack depth counters (would require new fields on ExecutionFrame).

Validation.

  • cargo +1.92.0 fmt --check
  • cargo +1.92.0 clippy --all-targets --all-features -- -D warnings
  • cargo +1.92.0 test --all-features ✅ (578 lib + 249 integration)
  • cargo +1.92.0 build --release ✅ (asserts compile out)

No real bugs surfaced. Two initially-stronger invariants tripped existing tests and were correctly weakened — both were over-specifications on my part, not VM bugs (see commit message).

Independent of the storage-abstraction stack — opens against upstream/main.

@anakrish

anakrish commented Jun 2, 2026

Copy link
Copy Markdown
Owner Author

@copilot Review this PR using the review skills in the repo. Use a separate agent for each skill.

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR adds debug-mode invariant checks throughout the RVM to make stack/context/register lifecycle assumptions executable (and therefore test-enforced) during debug runs, while compiling out in release builds. It also updates several dependency versions (notably serde_json and spin) across the workspace and bindings.

Changes:

  • Add debug_assert!-based postconditions for reset_execution_state and per-dispatch-loop VM invariants.
  • Add targeted debug assertions around rule/comprehension stack balance and iteration advancement correctness.
  • Bump serde_json (and some related transitive deps) plus spin versions across the core crate and multiple bindings.

Reviewed changes

Copilot reviewed 10 out of 16 changed files in this pull request and generated no comments.

Show a summary per file
File Description
src/rvm/vm/state.rs Adds debug-only state clean postcondition checks and per-opcode VM invariant assertions.
src/rvm/vm/rules.rs Adds debug assertions to catch call-rule stack mismatches/underflows and rule finalize invariants.
src/rvm/vm/execution.rs Invokes VM invariant checks inside dispatch loops; adds debug preconditions for suspendable entry and resume.
src/rvm/vm/context.rs Adds debug assertions to catch invalid/overflowing iteration advancement in IterationState.
src/rvm/vm/comprehension.rs Adds debug assertion to catch ComprehensionEnd reached with an empty comprehension stack.
Cargo.toml Updates core dependency versions (notably serde_json, spin).
Cargo.lock Updates locked dependency graph to match the version bumps.
bindings/wasm/Cargo.toml Bumps serde_json and wasm-bindgen-test versions for the WASM binding.
bindings/wasm/Cargo.lock Updates WASM binding lockfile to match dependency bumps.
bindings/ruby/Cargo.lock Updates Ruby binding lockfile to match dependency bumps.
bindings/python/Cargo.toml Bumps serde_json version for the Python binding.
bindings/python/Cargo.lock Updates Python binding lockfile to match dependency bumps.
bindings/java/Cargo.toml Bumps serde_json version for the Java binding.
bindings/java/Cargo.lock Updates Java binding lockfile to match dependency bumps.
bindings/ffi/Cargo.toml Bumps serde_json version for the FFI binding.
bindings/ffi/Cargo.lock Updates FFI binding lockfile to match dependency bumps.

Copilot AI commented Jun 2, 2026

Copy link
Copy Markdown

@copilot Review this PR using the review skills in the repo. Use a separate agent for each skill.

Running both review skills now — code-review has completed (results below); deep-review is running its full Phase 1 → micro-pass → adversarial-verifier pipeline in a separate agent and I'll follow up with those results when it finishes.


code-review results

Inventory (11 items, all examined)

# Item File Risk
1 reset_execution_state (modified) state.rs:13
2 debug_assert_state_is_clean (new) state.rs:50 [A]
3 assert_vm_invariants (new) state.rs:116 [A][L]
4 jump_to (modified) execution.rs:115 [L]
5 execute_suspendable_entry (modified) execution.rs:192
6 resume (modified) execution.rs:207 [A]
7 run_stackless_loop (modified) execution.rs:300 [L]
8 execute_comprehension_end_run_to_completion (modified) comprehension.rs:607
9 IterationState::advance (modified — const fn) context.rs:54 [T]
10 finalize_call_rule_run_to_completion (modified) rules.rs:277
11 finalize_rule_suspendable (modified) rules.rs:836

Findings

LOW-1 · debug_assert_eq! argument labels are inverted relative to the custom message

Location: src/rvm/vm/rules.rs:280–284

debug_assert_eq!(left, right, ...) prints "left != right" in its auto-generated failure header. Here left = call_context.rule_index (the stack value) and right = rule_index (the function parameter). The custom message then says "expected rule_index {rule_index} got {call_context.rule_index}" — swapping the roles. A developer reading a failure will see the macro's built-in line with the stack value on the left, then the custom message with it on the right, requiring mental gymnastics to reconcile the two.

debug_assert_eq!(
    call_context.rule_index, rule_index,          // left = stack, right = param
    "call_rule_stack pop mismatch: expected rule_index {} got {}",
    rule_index, call_context.rule_index,           // param first, stack second (swapped)
);

Fix: Swap the debug_assert_eq! operands so the macro's built-in output reads "param != stack_value", matching the English "expected … got …" ordering of the custom message.


LOW-2 · Magic constant 4096 for execution-stack depth bound is undocumented

Location: src/rvm/vm/state.rs:150–154

The bound 4096 has no named constant, no citation of the deepest nesting observed in the test suite, and no guidance for operators if a legitimate deeply-recursive policy ever trips it.

debug_assert!(
    self.execution_stack.len() <= 4096,
    "vm invariant: execution_stack depth ({}) exceeds sanity bound",
    self.execution_stack.len(),
);

Fix: Define a named constant (e.g., const DEBUG_MAX_EXECUTION_STACK_DEPTH: usize = 4096) with a comment noting the empirical ceiling observed in testing.


Design Notes

  • Redundant double-check on Suspendable entry path. execute_entry_point_by_{index,name} in Suspendable mode calls reset_execution_state() (postcondition: debug_assert_state_is_clean()) then immediately calls execute_suspendable_entry() (precondition: debug_assert_state_is_clean()). No mutable call between them can disturb the checked fields. The double-check is harmless and the two calls document distinct semantic roles ("reset is complete" vs "entry-point precondition holds"). Intentional and defensible.

  • const fn + debug_assert! is safe here. The two new assertions in IterationState::advance use only literal string messages (no format args), which compiles to panic!("literal") — valid in const fn since Rust 1.57. The risk is latent: if a future editor adds format args (requires ≥ 1.73) while no MSRV is pinned in Cargo.toml, it would surface as a compile error, not silent wrong behaviour.


Summary

0 critical, 0 high, 0 medium, 2 low. All 157 insertions are pure debug_assert!/debug_assert_eq! gated by #[cfg(debug_assertions)], with zero release overhead. The two Low findings are cosmetic: an inverted argument order in a format string (LOW-1) and a magic number that would benefit from a named constant (LOW-2). Neither is a correctness or security issue.

@copilot Review this PR using the review skills in the repo. Use a separate agent for each skill.

deep-review results

Full three-phase pipeline: 3 parallel discovery agents → type-conversion + API-steward micro-passes → adversarial verifier.


Findings

MEDIUM-1 · Debug-only ComprehensionEnd assert reintroduces panic on malformed public bytecode

Source: Adversarial Verifier (confirmed) | Location: src/rvm/vm/comprehension.rs:610

execute_comprehension_end_run_to_completion() now executes a debug_assert! before the existing recoverable underflow path. Malformed bytecode reaching Instruction::ComprehensionEnd with an empty comprehension stack will panic in debug builds rather than returning VmError::InvalidIteration.

Program exposes public instructions and RegoVM::load_program() accepts arbitrary programs, so a caller can construct a program with a standalone ComprehensionEnd.

// NEW — fires before the recoverable path
debug_assert!(
    !self.comprehension_stack.is_empty(),
    "ComprehensionEnd reached with empty comprehension_stack at pc {}",
    self.pc
);
// OLD — still present, now unreachable when the assert fires
self.comprehension_stack.pop().map_or_else(
    || Err(VmError::InvalidIteration { ... }),
    |_context| Ok(()),
)

Trace:

program.instructions = vec![Instruction::ComprehensionEnd {}]
vm.load_program(Arc::new(program)); vm.execute()
→ expected: Err(VmError::InvalidIteration { .. })
→ actual (debug build): panic at the new assert

Fix: Remove the pre-pop debug_assert! on the comprehension stack here, or pop first and assert on the result:

match self.comprehension_stack.pop() {
    Some(_) => Ok(()),
    None => {
        debug_assert!(false, "ComprehensionEnd with empty comprehension_stack at pc {}", self.pc);
        Err(VmError::InvalidIteration { value: ..., pc: self.pc })
    }
}

This preserves the typed error for release and still fires the assertion in debug builds.

The companion debug_assert! in rules.rs::finalize_rule_suspendable (line 841) has the same structure — assert then graceful error — and should be reviewed with the same lens.


Dropped Candidates

  • resume() misuse panic — the new guard is debug_assert!-only; release builds still return VmError::InvalidResumeState.
  • 4096 execution-stack ceilingdebug_assert!-only, not a production execution limit.

Agent Performance

Agent Model Findings
A — Broad Scanner gpt-5.4 2 candidates
B — Value-Flow Tracer claude-opus-4.6 0
C — Safety/API Specialist default 0
Type-conversion micro-pass 0
API-steward micro-pass 0
Adversarial Verifier confirmed 0, dropped 2, found 1 new

Summary

1 finding (0 critical, 0 high, 1 medium, 0 low). The diff is well-executed defensive instrumentation, but the comprehension.rs pre-pop debug_assert! changes the behavior of malformed-program execution from typed error to panic in debug builds. All other assertions correctly follow the assert-then-graceful-error pattern.

@anakrish
anakrish force-pushed the storage-abstraction-vm-invariants branch from 9da97d9 to 9b7e04d Compare June 2, 2026 16:35
@anakrish

anakrish commented Jun 2, 2026

Copy link
Copy Markdown
Owner Author

Thanks — all three are legitimate. Fixed in 9b7e04d:

  • MEDIUM-1 (comprehension.rs): dropped the pre-pop debug_assert!. RegoVM::load_program accepts user-supplied programs, so a standalone ComprehensionEnd must surface as VmError::InvalidIteration in both debug and release — the existing typed-error path is the correct contract. The companion assert in rules.rs::finalize_rule_suspendable had the same pattern and got the same treatment.
  • LOW-1 (rules.rs:280-284): swapped operands so the macro's auto-generated left != right line matches the "expected … got …" custom message.
  • LOW-2 (state.rs:150): hoisted to DEBUG_MAX_EXECUTION_STACK_DEPTH with a doc comment clarifying it's a debug sanity net, not a production limit.

cargo +1.92.0 fmt, clippy --all-targets --all-features -D warnings, and test --all-features (578 lib) all green.

@anakrish
anakrish force-pushed the storage-abstraction-vm-invariants branch from 9b7e04d to 095ce64 Compare June 2, 2026 16:42
@anakrish

anakrish commented Jun 2, 2026

Copy link
Copy Markdown
Owner Author

@copilot Review this PR using all the review skills in this repo. Use a separate agent for each skill.

Copilot AI commented Jun 2, 2026

Copy link
Copy Markdown

@copilot Review this PR using all the review skills in this repo. Use a separate agent for each skill.

Both review skills completed. Full reports at /tmp/code-review-report.md (inline below) and /tmp/deep-review-report.md.


code-review results

1 finding (0 critical, 1 high, 0 medium, 0 low)

HIGH · resume() debug_assert panics before typed error path

Location: src/rvm/vm/execution.rs:212
Confidence: High

The new debug_assert! fires before the existing match arm that returns VmError::InvalidResumeState. In a debug build, any caller (including FFI consumers) that calls resume() with non-Suspended state gets a panic instead of the typed error. That panic can propagate across the C FFI boundary and permanently poison the process-global FFI state via with_unwind_guard().

pub fn resume(&mut self, resume_value: Option<Value>) -> Result<Value> {
    debug_assert!(                                     // ← fires first, panics
        matches!(self.execution_state, ExecutionState::Suspended { .. }),
        "resume precondition: ...",
    );
    let (reason, mut last_result) = match self.execution_state.clone() {
        // ...
        current_state => return Err(VmError::InvalidResumeState { .. }),  // now unreachable
    };

Fix: Remove this debug_assert! (or move it after the match so invalid states still return VmError::InvalidResumeState in all build profiles). The caller-misbehaviour contract is already enforced by the typed error — the assertion duplicates that contract while breaking it in debug mode.


deep-review results

2 confirmed findings (1 critical, 1 high)

CRITICAL · resume() panics instead of returning typed error in debug builds

Location: src/rvm/vm/execution.rs:212
Confidence: High (confirmed by adversarial verifier)

Same as above. The adversarial verifier independently confirmed: the debug_assert! fires before VmError::InvalidResumeState can be returned, converting a recoverable API-misuse error into an unrecoverable panic that can cross the FFI boundary.


HIGH · DEBUG_MAX_EXECUTION_STACK_DEPTH = 4096 can panic on legitimate deeply-nested programs in debug builds

Location: src/rvm/vm/state.rs:168
Confidence: Medium

assert_vm_invariants() fires a debug_assert! every time around the dispatch loop when execution_stack.len() > 4096. Rego policies with deep mutual recursion or large comprehension nesting can legitimately exceed this in debug builds, causing the test suite or fuzz harness to fail with a panic rather than a policy-evaluation error. Since the code comment already describes this as "a debug-only sanity net, not a production limit," it should be documented/defended more explicitly — or the constant should be raised to something clearly unreachable in practice (e.g. 65536).

Evidence:

const DEBUG_MAX_EXECUTION_STACK_DEPTH: usize = 4096;
// ...
debug_assert!(
    self.execution_stack.len() <= DEBUG_MAX_EXECUTION_STACK_DEPTH,
    "vm invariant: execution_stack depth ({}) exceeds sanity bound ({})",
    self.execution_stack.len(), DEBUG_MAX_EXECUTION_STACK_DEPTH,
);

Fix: Either raise the constant well above any legitimate policy depth, or add a test showing the deepest observed nesting in the suite and gate the constant off that.


Dropped candidates (adversarial verifier)

  • Pre-pop debug_assert! in comprehension.rs — already fixed in 9b7e04d
  • finalize_rule_suspendable companion assert — same fix applied ✅

Summary: The resume() finding is the only one that affects the external contract. Both reviewers agree on the fix: remove (or reposition) the debug_assert! so VmError::InvalidResumeState remains reachable in debug builds. The 4096 depth bound is lower-severity and can be addressed by documentation or raising the constant.

@anakrish
anakrish force-pushed the storage-abstraction-vm-invariants branch from 95cda71 to 095ce64 Compare June 2, 2026 20:36
@anakrish
anakrish changed the base branch from main to upstream-main-snapshot June 2, 2026 20:36
@anakrish
anakrish force-pushed the storage-abstraction-vm-invariants branch 4 times, most recently from 1662571 to fb31788 Compare June 4, 2026 15:45
Encode VM stack/context/register lifecycle invariants as
debug_assert!s. Zero cost in release; surfaces violations during
debug-mode tests and CI.

Invariants covered:
- reset_execution_state postcondition: all stacks empty, registers
  resized to base and Undefined, rule_cache reset, pc/executed
  counters zeroed, builtins_cache cleared, execution_state Ready.
- Per-opcode invariant check (assert_vm_invariants) invoked at the
  top of run_stackless_loop and jump_to iterations: state is
  Ready/Running, registers non-empty, rule_cache sized to program,
  execution stack bounded by a debug-only sanity ceiling
  (DEBUG_MAX_EXECUTION_STACK_DEPTH = 4096; not a production limit).
- resume() precondition: execution_state is Suspended.
- execute_suspendable_entry precondition: clean state (callers reset
  immediately before).
- Rule finalize: call_rule_stack pop matches the finalized rule_index.
- IterationState::advance: Single iterator not advanced past
  consumption, Array index not at usize::MAX before saturating_add.

All assertions are gated by #[cfg(debug_assertions)] (directly or via
debug_assert!) so release builds are unaffected.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
@anakrish
anakrish force-pushed the storage-abstraction-vm-invariants branch from fb31788 to 4c42093 Compare June 4, 2026 16:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants