What each of your declarations cost, measured in reductions.

ExTLA.Coverage answers how often the checker asked a declaration. This answers how expensive the answer was — the other half of the question a spec author has when a run is slow, and the only half they can act on. "Invariant checking is 3.2%" is a fact about the checker; "quorum_agrees cost 2,400 reductions each of 58,359 times" is a fact about the spec in front of them.

Why reductions and not milliseconds

A wall-clock number means nothing without the CPU model and the load average it was taken under: the same model-checking run can swing by a quarter or more on machine load alone.

A reduction is the BEAM's own unit of work. The counter is incremented on function calls and BIF work and consults neither the clock nor the CPU, so the count is a function of (OTP version, code, data) and of nothing else. The same fixed workload under 32 competing processes:

wall       2,512 -> 5,032 µs, a 100.3% spread
reductions 225,017 -> 225,017

The floor is the measurement, and the total is not

Accumulating the deltas does not give a reproducible number. Eight runs of one spec under 32 competing processes, totals:

invariant  19 reds/eval     3,819 -  4,839    26.7% spread
invariant  34 reds/eval     6,834 -  7,249     6.1%
guard       2 reds/eval       402 -    594    47.8%

The excursions are absolute — a reduction or five on some evaluations — so they are negligible against an expensive declaration and total against a cheap one. Ranking on those totals gave five different orders in ten runs.

The per-evaluation minimum has no such problem. Across the same eight loaded runs every declaration's floor came back a single value — 3, 11, 20, 35, 80, 155, 305 — with zero variance. That is the honest reading of what is happening: the floor is what the predicate costs, and anything above it in a given evaluation is the scheduler getting in the way of the measurement rather than the predicate doing more work.

So the reported cost is floor x evaluations. That is reproducible to within a small absolute margin — two reductions per evaluation — and the margin does not grow with load. A floor can only be pushed up, by an evaluation that never ran uninterrupted, so a short run on a busy machine may miss the true minimum and land a reduction or two high; it cannot land low. On a 304 reds/eval declaration that is 0.7%, and it is still two reductions at load 32, where the same workload's wall time spread 100.3%. Evaluation counts are exact under any conditions — they are a function of the search, not of the measurement.

What the floor cannot see is a predicate whose cost genuinely varies with the state — one that short-circuits on most states and does the work on a few. Its floor is the cheap case, so the reported cost understates it. That is why observed is kept beside it and why the report flags a row whose observed total runs well above its attributed one: the gap is a finding, not a defect, and averaging it away would hide the most interesting predicate in the spec.

What this deliberately does not measure

Garbage collection. Reductions do not charge for it, so a predicate that allocates heavily is slightly undercharged — measured at ~2% of wall on an allocation-heavy loop, against the 30% the wall clock swings on load. The trade is worth it and is stated rather than hidden.

The checker's own machinery. Its phases are ETS and NIF work rather than user code, and whether reductions describe those well is a question nobody has measured. This module wraps the closures ExTLA.Spec.Compiled holds and nothing else.

Where the window opens and closes, and why there is no bounded_by here

The window is the search, and only the search. The checker instruments a copy of the spec for the search and stops counting when that copy stops being called; the state graph keeps the uninstrumented spec, because everything that consults it runs after the search has stopped — replay, which turns an ExTLA.StateGraph.path_to/2 result back into states by applying transitions. Regenerating a counterexample, or materializing every state so a liveness predicate can be evaluated over it, is not work the spec's transitions did while exploring. Counting it would charge a refuted run each trace step twice, and a check_liveness: true run roughly a whole second search.

That boundary is what lets this module say something ExTLA.Coverage cannot. Coverage's bounded_by exists because a halted search leaves the state space incompletely described: its counts are a floor on a question about the spec. This module's counts are not a claim about the state space at all — they are a census of work performed, and a search that halted performed exactly the work it performed, its partial last expansion included. That number is complete under every halt condition, so there is deliberately no bounded_by on a profile: it would qualify a count that is not uncertain.

A reader who needs to know the run stopped early has status and coverage.bounded_by on the same result struct, which is the honest place for it.

Why the process dictionary

The closures are called from deep inside the checker's hot path — invariant checking, guard evaluation, action application — and they return only their value. There is nothing to thread an accumulator back through, short of changing the signature of every call site in the hot path to carry one.

The dictionary is not merely the convenient answer, it is the correct boundary: it is per-process, which is exactly what a worker's contribution is under workers: (each worker's ExTLA.Coverage starts from zero for the same reason). A worker reads its own dictionary at the end of its slice and hands back a struct, so merge/2 composes the way ExTLA.Coverage.merge/2 does and no shared mutable state touches the expansion path.

Writes are confined to bump/2 and reads to collect/1. Nothing else in the project reads these keys.