CLAUDE.md@packages/statem · git:20261017.e57cc7b · 2026-10-17 · sha256 4b79ba5090e5f741
CLAUDE.md@packages/statem git:20261017.e57cc7bA
Immutable. This exact content never changes and is served at /api/v1/blob/4b79ba5090e5f741.
# statem
## Purpose
Stateful, model-based property testing on qcheck. A test describes a system
as a `Spec` (abstract model, command generator, precondition, pure
`next_model`, and an `execute` hook that runs a command on the real system
and checks it); `statem.check` generates admissible command lists, runs them,
and shrinks a failing list to a short one that fails the same way. It is a
testing library: consumers take it as a dev dependency
(`statem = { path = "../statem" }`). Nothing in `src` performs I/O.
Portable by rule. No `@external`, no `gleam_erlang`/`gleam_otp`, no `panic`
or `let assert` in `src`: R6 holds this package to the same subset as
`core`, `machine`, `prompt` and `session_view` (`lint/policy.portable_packages`),
and its tests pass on both `--target erlang` and `--target javascript`.
Dependencies are `gleam_stdlib`, `gleam_yielder`, `qcheck` and `exception`
(the last is JS-capable, already qcheck's own dependency, and is how a crash
in a consumer callback is caught).
## Key types
One module, `statem`.
- `Spec(model, cmd, sut)` is a record of functions: `initial`, `command`,
`precondition` (returns `Admission`, `Admit | Reject`), `next_model`
(pure, symbolic), `new_sut` (one fresh system per execution), `execute`
(`fn(sut, model_before, cmd) -> Result(sut, Violation)`), `finish` and
`teardown`. Commands are plain data, never closures. `new_sut`, `execute`
and `finish` run under `exception.rescue`: a crash is a `Violation` tagged
`statem.crash`, which shrinks like any other (same-tag rule).
- `Violation(tag, detail)`. Shrinking accepts a candidate only if it fails
with the original tag, so two bugs need two tags.
- `Config(test_count, seed, max_commands, max_shrinks, shrink_retries,
shrink_stop)` via
`default_config(seed:)` and `with_*` (`with_shrink_retries(n)`, default 1:
a candidate still fails if any of n executions fails with the original
tag; retries spend `max_shrinks`; `with_shrink_stop(fn() -> ShrinkStop)`,
`KeepShrinking | StopShrinking`, default always keep). There is no random
default seed.
- `Failure(cmd)` carries seed, run index, violation, original and shrunk
lists, failing step, shrinks accepted, candidates run, and `ShrinkEnd`
(`ShrinkConverged | ShrinkBoundHit`).
- `check`, `check_run` (one run from `(seed, run)` alone), `commands` (the
list run `i` generates, nothing executed; equals that run's
`Failure.original`), `replay` (one
exact list; an inadmissible list is a `statem.precondition` violation),
`report` (multi-line text for a `panic as`).
## How it works
Run `i` draws its list from the `i`th 32-bit draw of a qcheck stream seeded
with `config.seed`, so the derivation is integer-exact on both targets for any
seed (seeds equal modulo 2^32 collide, qcheck's own limit); `check` threads
the stream, `check_run` and `commands` walk it. The generator is a
hand-written `qcheck.Generator` threading the seed and the model, keeping
each command's whole shrink tree; a rejected draw is retried up to eight
consecutive times, then the list ends early. It never uses `qcheck.bind`,
which regenerates downstream values on a shrink.
Shrinking is its own greedy loop. The whole-list deletion is offered once,
first. Then each round tries deleting a contiguous chunk of n/2, n/4, ..., 1
commands (a halving schedule, not every size) at every offset, then replacing
one command by a child of its shrink tree. Candidates are replayed through
the preconditions from `initial` and dropped unexecuted if any rejects. Only
executions spend `max_shrinks` (each retry too); inadmissible candidates are
free against it but capped at a fixed 250000 per shrink so an infinite
hand-built tree terminates. Either bound ending the search with an
admissible candidate untried is `ShrinkBoundHit`. The caller's `shrink_stop`
predicate is a third bound: R6 keeps a clock out of this package, so a test
whose candidates cost wall time closes over a monotonic deadline and answers
`StopShrinking`; it is asked just before each execution (the whole-list
candidate included, never the initial failing run, never a dropped
candidate), and the best list so far is reported as `ShrinkBoundHit`. The search is one
self-tail-recursive function (`search`): a mutual recursion costs a stack
frame per candidate on JavaScript and overflowed on wide trees.
## Invariants that break things
- `execute` receives the model BEFORE the command; `next_model` is applied
by the driver, never by `execute`.
- `new_sut` must return a system sharing nothing with earlier ones; it is
called once per run and once per shrink execution. `teardown` runs on every
path where a system exists, crashes included, and never escapes (its own
crash is discarded). When `execute` returns `Error` or crashes, `teardown`
receives the last good system, the one BEFORE the failing command.
- Commands that name state by value shrink badly (deleting the creator
makes users inadmissible); name state by index or position.
- Call counts of `new_sut`/`teardown` are not observable in a package that
may not use `@external`; the tests check freshness through a per-system
step counter instead. The retry policy lives in `statem/internal/retry`,
a pure function taking an injected `run(attempt_index)`, so tests drive it
with a `run` that fails on chosen attempts; no test needs FFI.
- Not built, deliberately: parallel runs and linearizability, symbolic
result variables, statistics, env-var seed overrides, a `qcheck.run`
adapter, a `shrink_cmd` hook.