feat(state-machine): persist shrunk transition sequence, not just the seed - #653
Draft
nightscape wants to merge 6 commits into
Draft
feat(state-machine): persist shrunk transition sequence, not just the seed#653nightscape wants to merge 6 commits into
nightscape wants to merge 6 commits into
Conversation
… seed Adds an optional `persistence` feature to proptest-state-machine that writes the minimal (shrunk) failing case of a state-machine test to disk as serialized `(initial_state, Vec<Transition>)`, and can replay it directly without regenerating from a seed or re-running the shrinking process. Motivation (issue proptest-rs#564): proptest's built-in failure persistence stores only the RNG seed. Replaying it must regenerate the case from the strategy and re-shrink, and it silently breaks when the reference model or transition strategy changes. State-machine transitions, unlike a generic proptest Value, are concrete user types that can implement serde, so the failing case can be persisted verbatim. - `persistence` module: `PersistedCase<S, T>` (serde), save/load, env-var config (`PROPTEST_STATE_MACHINE_PERSIST_DIR`, `PROPTEST_STATE_MACHINE_REPLAY`), and a `CaptureGuard` that writes on unwind (last-write-wins yields the shrunk case since proptest re-runs the body for each shrink candidate). - `StateMachineTest::test_sequential_persisted` and the `prop_state_machine_persisted!` macro as opt-in drop-in replacements. - proptest core: don't warn on the reserved `PROPTEST_STATE_MACHINE_*` env-var namespace. - Integration test covering capture+shrink, replay, and the no-write-on-pass path. Feature is fully additive and gated; default builds are unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
nightscape
commented
Jun 24, 2026
nightscape
commented
Jun 24, 2026
nightscape
commented
Jun 24, 2026
…ither/or Addresses review feedback on the persistence feature: - Persisted regressions are now replayed on *every* run before generating new cases (mirroring proptest's seed-regression behaviour), instead of an env-var-gated "replay OR generate" mode. `prop_state_machine_persisted!` calls the new `StateMachineTest::replay_persisted_regressions` once per run, then runs the normal generation loop. `PROPTEST_CASES=0` replays the regression alone. Removes `PROPTEST_STATE_MACHINE_REPLAY`. - Reword the module docs to describe the durable seed-vs-case trade-off rather than a transient "what proptest does today", and drop the GitHub issue link from the source (kept in CHANGELOG/PR). - Add an end-to-end test exercising the macro (replay no-op + generation). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Per review: distinct failures (not shrunk versions of each other) must be kept, not overwritten. The persisted file is now a JSON *array* of cases: - Within a run, successive shrink writes replace this run's previous entry (tracked by a per-(test,thread) marker reset at the start of each run via `replay_persisted_regressions`), collapsing to the single minimal case. - Across runs, a distinct minimal is appended; exact duplicates are de-duped. Subsequence-based subsumption is intentionally avoided — two different bugs can be subsequence-related, so it could drop a distinct regression. The replay-before-generate flow already prevents accumulating two shrinks of the same live bug. `replay_persisted_regressions` now replays the whole set in order. Adds a unit test of the merge logic and an end-to-end test that accumulates two distinct minimal cases and de-dupes a re-discovery. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Switch the persisted regression file from a pretty-printed JSON array to JSON Lines (one compact case per line, under a `#` comment header), matching proptest's line-oriented seed-regression files. One case per line gives clean per-regression diffs and union-friendly merges in source control. Drops the per-case `note` field in favour of the file header; `.json` -> `.jsonl`. Reads skip blank/`#` lines; a malformed case line is a hard error on the replay path. Adds an on-disk-format assertion to the capture test. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Persistence keeps a single, uniform serde requirement on both `State` and `Transition`. Document that a large / not-directly-serializable state can persist a compact, reconstructible payload via `#[serde(into, from)]` rather than needing a bespoke state-codec abstraction (which would be asymmetric with `Transition` and redundant with serde's own proxy support). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
nightscape
force-pushed
the
feat/state-machine-persisted-transitions
branch
from
June 24, 2026 22:30
fce50c2 to
fb03da0
Compare
Separate the persistence module into two layers:
- `persistence::store` — StateMachineTest-agnostic: JSON Lines I/O, the
accumulate/de-dup merge, the per-run marker, and the panic `CaptureGuard`,
generic over any `Serialize + DeserializeOwned` case type. `CaptureGuard::new`
becomes `CaptureGuard::arm(path, &case)` taking an already-built case.
- `persistence` (mod.rs) — the thin StateMachineTest glue: `PersistedCase`,
`default_persist_path`, `load_set`, re-exporting `store::{reset_run_marker,
PERSIST_DIR_ENV}`.
No behavior change (all tests green). This makes the store reviewable in
isolation and reusable by projects with a richer fixture type than
`PersistedCase`, without a bespoke per-project reimplementation.
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
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.
Persist the shrunk transition sequence, not just the seed (proptest-state-machine)
Closes #564. Related context: #440.
Problem
Proptest's built-in failure persistence stores the RNG seed of the failing
TestRunner. For state-machine tests that has two costs:strategy and then re-runs the whole shrinking process before the minimal
counter-example is reached.
strategy changes, the same seed no longer maps to the same case, so the
stored regression silently stops pinning the bug it was meant to pin.
Issue #564 asks for the ability to save and load the fully-shrunk failing
case directly. Unlike a generic proptest
Value, a state-machine failing caseis a concrete, human-readable value —
(initial_state, Vec<Transition>)— thatcan usually implement
serde::Serialize. That makes the state-machine crate thenatural home for this (proptest core stays seed-based and untouched apart from a
one-line env-var namespace reservation).
What this adds
A new opt-in
persistencefeature (pulls inserde+serde_json).The model mirrors how proptest treats seed regressions: persisted cases are
replayed on every run, and freshly generated cases run on top to keep
finding new failures. Distinct failures accumulate into a regression file
stored as JSON Lines (one case per line, like proptest's line-oriented
seed-regression file — clean diffs and union-friendly merges in source control),
while shrunk versions of the same failure collapse to one minimal case.
prop_state_machine_persisted!— macro counterpart ofprop_state_machine!.It expands to a test that (1) calls
replay_persisted_regressionsonce perrun, then (2) runs the normal generation loop with capture-on-failure.
StateMachineTest::replay_persisted_regressions(config)— loads the persistedcase (if any) and re-runs it via
test_sequential. A still-failing regressionpanics here, attributed to the stored case rather than to a generated one.
StateMachineTest::test_sequential_persisted(...)—test_sequentialpluscapture-on-failure.
persistence::PersistedCase<S, T>— the on-disk case shape(
{ initial_state, transitions }); the file is one such object per line(JSON Lines) under a
#comment header.persistence::store— theStateMachineTest-agnostic half: JSON Lines I/O,the accumulate/de-dup merge, the per-run marker, and the panic
CaptureGuard,generic over any
Serialize + DeserializeOwnedcase type. The trait/macroglue is a thin layer on top. Factored out so it's reviewable in isolation and
reusable by projects with a richer fixture type; happy to narrow its
visibility if you'd prefer a smaller public surface.
persistence::CaptureGuard— an RAII guard that serializes the case eagerlyand, on unwind, merges it into the regression set. Within a run, proptest
re-runs the body for every shrink candidate; successive writes replace this
run's previous entry (collapsing to the minimal). Across runs, a distinct
minimal is appended; exact duplicates are de-duplicated.
PROPTEST_STATE_MACHINE_PERSIST_DIRenv var overrides the persistencedirectory (default
proptest-regressions/state-machine).PROPTEST_CASES=0replays the regression without generating new cases.
PROPTEST_STATE_MACHINE_*namespace is reserved so theconfig env scanner doesn't print
Ignoring unknown env-var.The reference
StateandTransitionmust implementserde::Serialize + serde::de::DeserializeOwnedto use the persisted path; thebase traits are unchanged, so existing tests and default builds are completely
unaffected.
Usage
On failure the shrunk sequence is written to
proptest-regressions/state-machine/<type>.jsonland committed like a normalregression file. Every subsequent run replays the stored cases first, then
generates new cases. To replay only the regressions (no new generation):
PROPTEST_CASES=0 cargo test my_testTests
proptest-state-machine/tests/persistence.rs:file contains the minimal shrunk sequence (exactly four increments), not
an unshrunk one;
replay_persisted_regressionsreproduces the failure from that file;prop_state_machine_persisted!exercises themacro (replay no-op + generation) end to end;
across runs, and re-discovering one already stored does not duplicate it
(plus a focused unit test of the set-merge logic).
Notes / open questions for maintainers
exact-equality de-dup, not by subsequence subsumption. Subsumption would be
unsound here: two genuinely different bugs can be subsequence-related, so
collapsing by subsequence could silently drop a distinct regression. Instead,
the replay-before-generate flow already prevents accumulating two shrinks of
the same live bug (its regression fails replay before generation can run),
and within-run shrinking collapses to one minimal. If you'd still like
same-bug-across-strategy-change collapsing, we'd need a per-failure identity
signal (e.g. the panic message) — happy to explore.
State: Serializeand no bespoke abstraction? Persistence is a single,uniform serde requirement on both
StateandTransition— no special-casingof one over the other. A state that is large or not directly serializable can
persist a compact, reconstructible form via
#[serde(into = "…", from = "…")](documented in the module docs), so the serde bound isn't a hard ceiling. I
deliberately avoided a dedicated state-codec trait: it would be asymmetric with
Transitionand is redundant with serde's own proxy support for any state youown. If foreign (orphan-rule-blocked) states create real demand later, a codec
can be added additively.
through the
fork/timeoutout-of-process runners. Happy to gate or documentthat explicitly.
serde_jsonwas chosen for human-readability (these files are meantto be inspected and checked in). If you'd prefer a different format or to make
the serializer pluggable, easy to change.