feat(test): move stateful coverage to proptest-state-machine

[zerosnacks]

Summary

Move Steda's PostgreSQL stateful test suite fully onto proptest-state-machine and replace the previous hand-rolled generated-history runner with an explicit reference model and state-machine SUT.

The new harness keeps the strongest parts of the existing suite — real PostgreSQL execution, operation-level assertions, stale mutation checks, fake-time behavior, and invariant audits after every transition — while making generation and shrinking substantially more intentional.

What changed

• Replace the manual Vec<Operation> / TestRunner history runner with proptest-state-machine.
• Add a ReferenceStateMachine that tracks the minimum durable state needed to guide useful transition generation.
• Keep PostgreSQL as the concrete StateMachineTest implementation and retain one connection for the full generated case so the session-scoped fake clock remains stable.
• Preserve the aggregate stateful campaign diagnostics and per-transition trace support.
• Bias normal claims toward productive work and move empty-queue behavior into an explicit probe.
• Track conservative runnable and active-run state in the reference model so positive-path operations are not generated without evidence that they can succeed.
• Add explicit checkpoint replay coverage and assert first-write-wins/idempotent replay behavior.
• Separate stale checkpoint mutation coverage into a dedicated probe rather than relying on random stale selections.
• Preserve the existing SQL invariant audits and rejected stale mutation coverage.
• Remove the previous stateful execution path entirely; there is no parallel or legacy runner left.

Why

The previous stateful suite already exercised long randomized histories against the real database, but operation generation was largely state-oblivious and shrinking had no independent semantic model to work from.

Using proptest-state-machine gives the suite:

• state-aware transition generation;
• semantically coherent shrinking;
• an independent executable reference model;
• clearer separation between valid lifecycle operations and deliberate negative probes;
• better use of the transition budget.

The model is intentionally conservative. It does not attempt to mirror all PostgreSQL implementation details; it only tracks enough state to guide meaningful generation while the database and invariant audits remain the authoritative correctness checks.

Coverage

A representative 64-case run currently exercises roughly 4,000 transitions and includes:

• task creation and idempotent spawn replay;
• productive and explicitly empty claims;
• run completion and failure;
• retry-ready and scheduled retry paths;
• direct and policy-driven cancellation;
• lease expiry and reaping;
• supervision;
• sleep/suspension;
• checkpoint writes and explicit checkpoint replay;
• stale failure, completion, retry, checkpoint, sleep, and supervision mutations.

After making claims model-aware, natural empty claims dropped from hundreds per campaign to low double digits while explicit empty-claim probes continue to cover the negative contract.

Checkpoint replay generation is likewise state-aware now: successful explicit replays are exercised without spending transition budget on unavailable replay attempts.

Validation

make test-stateful passes with the full generated campaign, and the suite continues to audit PostgreSQL invariants after every transition.

Example result:

[stateful] PASS: 64 histories, 4136 generated transitions; PostgreSQL invariants and operation contracts held after every transition
[stateful] workload: generated_spawns=573 | idempotent_replays=286 | runs_claimed=449 (15 natural empty claims) | empty_claim_probes=74 | supervised_run_changes=29
[stateful] durable control: manual_retries=9 | checkpoint_writes=49 (2 incidental replay/skipped) | explicit_checkpoint_replays=7 (0 unavailable/skipped) | sleeps_suspended_or_cancelled=22 (2 ready/skipped)
[stateful] outcomes: tasks_completed=54 | completion_policy_cancellations=1 | direct_task_cancellations=147 | failed_runs=44 -> retry_ready=25, retry_scheduled=6, task_failed=11, task_cancelled=2
[stateful] maintenance: nonzero_time_advances=344/390 calls | expired_runs_reaped=41 across 186 sweeps | policy_cancellations=23 across 196 sweeps
[stateful] rejected mutations exercised against PostgreSQL: supervisions=42 | failures=325 | completions=372 | retries=203 | checkpoints=95 | sleeps=279
[stateful] no-op/skipped: supervision=119 | fail=0 | complete=0 | cancel_terminal_or_missing=164 | retry=0 | checkpoint=2 | checkpoint_probe=2 | checkpoint_replay=0 | sleep=2

This leaves Steda with one stateful testing path: a model-based proptest-state-machine harness driving the real PostgreSQL implementation.