git:20261018.ff57864 to git:20261019.d45df21

# 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

Two modules: `statem`, the sequential layer, and `statem/linearize`, the

pure linearizability checker the parallel layer (`packages/statem_parallel`)

uses as its oracle.

- `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.

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`).

## `statem/linearize`

`check(machine, initial, branches, budget)` decides whether the per-branch

histories of a concurrent run (`Event(cmd, response, invoked_at,

returned_at)`, instants in any one monotonic unit) merge into one order that

keeps each branch's order, respects real time (a call that returned

strictly before another was invoked goes first; equal instants overlap, the

safe reading for a coarse clock) and satisfies `Machine.postcondition`

against the model at every position. The answer is `Linearizable(order)`,

`NotLinearizable(Explanation)` (the deepest dead end: the longest placed

prefix and, for each branch's next call, `Violated(violation)` or

`Overtaken(branch, index)`) or `Undecided(nodes)` once `budget`

postcondition evaluations are spent. `Undecided` is a failure, never a

pass. The search is depth-first over each branch's next call, with a

memory of failed states keyed by branch positions and model (sound because

nothing else decides the future), so models must be comparable data. It is

pure, tested on both targets, and R6-clean like the rest of the package.

`statem` also exposes, for that layer and not to be built on lightly:

`run_seed`/`next_run_seed` (the per-run seed derivation), `grow` (the

model-threading command generator, returning `Grown(trees, model, seed)`),

`first_failure` and `Attempted` (the retry policy), and `crashed` (the

`statem.crash` violation).

## 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: running anything in parallel (that is

`statem_parallel`, which needs processes and so cannot live here),

symbolic result variables, statistics, env-var seed overrides, a `qcheck.run`

adapter, a `shrink_cmd` hook.