Skip to content

Report contract state before a failure with --snapshot - #277

Open
DicksonWu654 wants to merge 1 commit into
stx-labs:masterfrom
DicksonWu654:feat/failure-snapshot
Open

DicksonWu654 wants to merge 1 commit into
stx-labs:masterfrom
DicksonWu654:feat/failure-snapshot

Conversation

@DicksonWu654

@DicksonWu654 DicksonWu654 commented Oct 5, 2026 •

Copy link
Copy Markdown

Context

When an invariant fails in a stateful run, the shrunk counterexample shows the
calls but not the contract state that led to the failure, which makes the cause
hard to see. #145 asks for exactly this.

This implements #145 the way it was suggested in the issue: instead of
taking a snapshot on every run, Rendezvous replays the failing seed and
reads the state only after a failure.

With the opt-in --snapshot flag (config key snapshot), when a run fails
Rendezvous:

  1. resets the simnet session,
  2. replays the same seed, with the same options, up to the first failing
    run (stopping there, without shrinking or output), and
  3. prints the target contract's data variables before each call of that
    run, with the block heights:
Replaying seed 1 up to run 5 to report the state before the first failure...
Simnet session reset.

Contract state before each call of run 5, the first failing run (counter data variables only):

₿       ... Ӿ       ...   before test-below-limit
  counter: u4
  flag: false

For property tests the state is read right before the failing test function
is called. For invariant tests it is read before each public function call
of the failing run and before the invariant check, so the state changes can
be followed.

Cost: passing runs make no extra simnet calls and nothing is replayed. After
a failure, the replay runs the seed once more up to the failing run and
reads the variables only in that run. Without --snapshot, nothing changes.

Scope and limits:

  • Only the target contract's data variables (define-data-var) are shown,
    as Clarity values. Maps cannot be enumerated through the SDK; constants,
    token balances and other contracts are out of scope.
  • The state comes from the first failing run, before shrinking. With
    --bail, this is the run in the failure report; without it, the reported
    counterexample may be a shrunk version of that run.
  • If the replay does not fail at the same run (for example, a dialer
    behaves differently), Rendezvous says so and reports no state. A read
    error is reported instead of the state and does not change the replay.
  • The replay does not save the failure again for regression testing.
    --regr together with --snapshot reports the state for each failing
    regression.

Tests cover the recorder (only the target run is read, data variables only,
read errors are kept), the reporter (no replay for passing runs, no state on
a mismatched replay or read error), end-to-end property and invariant
failures in a temporary project (exact values before each call, no duplicate
regression record), and that passing runs and runs without the flag print no
state. The README and the Usage chapter document the option, config key and
output.

🤖 Generated with Claude Code

Add opt-in --snapshot (config key `snapshot`). When a run fails, reset
the session, replay the same seed up to the first failing run, and
print the target contract's data variables before each call of that
run. Passing runs do no extra work, as suggested in the issue, and
nothing changes without the flag. If the replay does not fail at the
same run, no state is reported.

Refs stx-labs#145.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

This branch has not been deployed

No deployments
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.

1 participant