**A minor line, opened by `mix extla.replay`.** It gains `--server` and `--timeout`, and
`--init-arg`, which was accepted and then dropped, now reaches the server (#165). That adds to
the command line, which is why this is 0.5.0 rather than 0.4.61. Nothing is removed or
renamed: a 0.4.0 project upgrades by changing the tag.
Two fixes reach spec authors. A function capture (`&abs/1`) in a spec body compiles (#369),
and `ExTLA.Invariant.Test.valid_states/3` says when a base generator is too broad to filter
(#348). The rest is how the project holds itself to its specification:
- spec/04's relation log ties each section to the tests that verify it and the code they
exercise, and gates CI (#336, now on surfex 0.7.1);
- `EXERCISE.md` records what the suite exercises in each shipped module (#370);
- the mutation sweep's kills are attributed to the mutant and reproduce on every seed (#378,
#380, #392);
- every CI job starts from a pinned base image and restores its dependencies from the store.
- **`mix extla.replay` passes `--init-arg`, `--server` and `--timeout` through** (#165).
The task declared `--init-arg`, so it was accepted, and then dropped: `ExTLA.Replay` was
called with no options, and its documented `:server` and `:timeout` were unreachable from
the command line. Now, with `--trace`:
- `--init-arg` is the argument the server starts with, as a literal Elixir term only
(`[start: 0]`; an expression is refused, never run);
- `--server` drives a running registered process instead of starting one, and leaves it
running;
- `--timeout` bounds each reply.
Whatever would otherwise be silently ignored is refused by name: `--init-arg` with
`--server`, an unregistered name or a printed pid, a non-positive timeout, and any of the
three with `--captured`, which drives nothing. `spec/05`'s holding note ("accepted and not
currently read") is replaced. `test/mix/switches_read_test.exs` now holds every task to
reading every switch it declares; against the old task it names `--init-arg`, and it finds
no other.
- **surfex 0.7.1** (#391, for #390). No upgrade step and no relation changed. Two lines in
CONTRIBUTING are corrected:
- **Running a section's tests:** `mix test --only verifies:<id>` doesn't select a test whose
tag is a list, because ExUnit compares a list as one string. `mix surfex.status` now counts
66 such tests, and for `mix extla.check`'s section `--only` runs 29 of its 39 tests.
CONTRIBUTING points to `mix surfex.test "<section id>"` instead.
- **Reviewing reached code:** a review now credits only the code the test calls, so the
review step for code reached through an entry point names that code with `--code`.
- **surfex 0.7.0** (#384, for #383). `verifies` tags now combine the way ExUnit merges them:
a test's own `@tag` replaces its describe's and module's, where surfex used to take their
union.
- **No relation changed.** Every test-level tag in spec/04's tests already repeated the
section it inherits, so `mix surfex.status` lists no Undeclared relations. With one
repeated id removed, status names that relation and fails.
- **Triangle gaps fall from 200 to 110.** The triangle now reads what a test calls from
source.
- `RELATIONS.md` and `PACKAGE_SURFACE.md` are regenerated.
- **Two of #354's stand-ins now use surfex reach** (#385, for #383). `ExTLA.ModelChecker.Safety`
implements its own section, and `ExTLA.ModelChecker.Parallel` implements Under `--workers`.
- **Evidence:** both are confirmed by evidence through `ModelChecker.run/2`, which their
tests drive, and each was reviewed with `mix surfex.validate`. The `run/2` `depends_on`
stand-ins, and `run/2`'s `implements` of the Safety section, are retired.
- **The other six keep their stand-ins.** They are reached only through a Mix task's
`run/1`, an undocumented `@impl` callback that reach doesn't follow (dco-tek/surfex#193).
CONTRIBUTING's row says so.
- **spec/04's relation log is baselined and gated** (#354, for #336). After green runs of all
three CI test slices, the baseline trusted 1,458 test versions and adopted 563 `verifies`
tags. 5 spec units have none. Every suggested `implements` citation was judged one at a
time and recorded with a note:
- 15 are confirmed by evidence, and one, the type `t:ExTLA.State.t/0`, by judgement;
- surfex counts only a direct call as a test exercising code. So 8 items reached only
through an entry point (a Mix task, or `ModelChecker.run/2`) are recorded as the entry
point implementing the section, plus a judged `depends_on`.
The new `relation-status-drift` job replaces the advisory `relation-evidence`. It is HARD,
and runs `mix surfex.status --verify`, the `RELATIONS.md` golden, and the evidence check.
It reads only the `test` job's evidence: no spec/04 tag is on a test only `docs` or
`mutation` runs, and GitLab intermittently loses those archives (#355). A test checks that
every golden's header, surfex's included, names a job that runs it.
- **surfex is pinned at `~> 0.6.2`** (#377, for #376). It makes `Surfex.Golden` and
`Surfex.SourceScan` supported, documented library API with a promise that their shapes and
`definition_hash/1` stay stable. All seven of extla's goldens are built on them, and none
changed but `PACKAGE_SURFACE.md`'s requirement row. For the spec/04 baseline (#354), it adds
recording that reads CI's evidence files (`--merge`), batched `confirm`/`validate` with a
distinct note per relation, and `suggest` in a deterministic order. No upgrade step.
- **CI restores dependencies with depdep v0.11.0** (#375, for #372). A correct restore is no
longer refused when a project's config sets a value a dependency read at compile time, and
`--explain-rebuilt` names the differing entry. Keys and schema are unchanged, so the store
needs no refill. The git-source restore it adds does nothing here: no dependency is git.
- **`EXERCISE.md` records what `mix test` exercises in each shipped module** (#370, for #323).
Nothing in the project could say whether a line ever ran; #323 found four that never had,
each by reading code. The `test` job now runs `mix test --cover --export-coverage test`,
and `mix extla.exercise --check` holds the new golden to that run in the same job, so
nothing is carried between jobs.
- **A row** is one module from `API_SURFACE.md`'s list: executable lines, unhit lines, and
the functions never entered.
- **The first run:** 310 of 3,892 lines unhit; the never-entered functions include
`ModelChecker.check_safety/1,2` and `Simulation.run/1` (listed on #323).
- **Stable:** three full runs gave identical coverage.
- **Accurate:** "never called" comes from per-function *line* coverage, because `:cover`'s
call counts miss a function that opens with `receive`. Macros, which run at their
caller's compile time, are excluded.
- **Gate ownership:** the rule that a golden's gate runs its `--check` now reads each
golden's own header, so `EXERCISE.md`'s `test` gate is enforced like `surface-drift`'s.
- **The n-ary product is written once** (#368, for #350). `ExTLA.Set.cross_many/1`,
`ExTLA.Function.record_set/1`, `function_set/2` and `ExTLA.Symmetry.mappings/2` each wrote
out the same fold, differing only in a seed and a combiner. They now call
`ExTLA.Product.fold/3`. `function_set(d, r)` is `record_set` with one range per key.
`ModelChecker.bindings/3` keeps its own: its later choices depend on earlier bindings.
- **Cost:** cheaper in every case, measured in reductions because the host's load makes
wall time noise. `function_set` is 13–26% fewer, `record_set` 21%, `cross_many` 23% (it
now folds the sets in reverse, so no tuple needs reversing), and `mappings` 8%. The
differential corpus, timed interleaved with `main`, shows no regression through that
noise.
- **Tests:** `test/ex_tla/product_test.exs` holds all four against a plain recursive
oracle, including the empty cases and `mappings`' order.
- **Guard:** `test/docs/product_shape_test.exs` refuses the fold's shape anywhere in `lib/`
but the two allowed sites. It was shown red on the old `ExTLA.Function`.
- **No shared test helper writes VM-global state, and the async-isolation gate checks them**
(#367, for #326). `test/docs/async_isolation_test.exs` read only each test file's own AST,
so a write one frame down in `test/support/` was invisible to it. `ExTLA.GuideCheck` set
`:ignore_module_conflict` for the whole VM, and the gate's claim held only because its two
callers were `async: false`.
- **The helper:** `GuideCheck` collects redefinition warnings with `Code.with_diagnostics/1`
instead, as #325 did for moduledoc examples.
- **The rule:** a module under `test/support/` cannot know whether its caller runs async, so
the gate now refuses any VM-global write there at all. That needs no call graph. It was
shown red on the old `GuideCheck`.
- **Arity:** entries carry it, because `Mix.shell/0` reads the shell and only
`Mix.shell/1` sets it. Matching by name alone would have flagged `extla.mutants`'s reads.
- **`ci-base-image` no longer runs on every new branch** (#374, for #373). Its `changes:`
rule had nothing to compare a branch's first push with, so GitLab counted every file as
changed and the job took a privileged runner on each work-item branch, only to find the
image already built. It now compares against `main` (`compare_to: refs/heads/main`), and
`ci_pipeline_test.exs` requires `compare_to:` on every `changes:` rule.
- **Tests that wait for an event no longer have a short deadline, and a short one must say
why** (#366, for #362). `cast_delivery_test`'s "a server that dies on the message is
reported" waited 1 s and missed it once on an oversubscribed host. A crashing server writes
its crash report before its `:DOWN`; measured, that takes a 0.3 ms median idle against 51 ms
(up to 188 ms) under CPU load and a log flood, and more on a host short of CPU.
- **Outcome waits are long.** The death case waits up to 30 s, and three more
death-waiting `assert_receive …, 1_000` drop their bound.
- **The default is long.** `test_helper.exs` sets `assert_receive_timeout: 5_000`, since
ExUnit's 100 ms default applied to every unbounded `assert_receive`. A passing wait
returns at its message, so a long bound costs nothing.
- **Short deadlines are justified.** `test/docs/deadlines_test.exs` requires a
`# deadline: <reason>` above any literal deadline under 5 s in `assert_receive`,
`refute_receive` or `Driver.deliver`. The three left are a timeout that is itself the
asserted outcome (×2) and a refute. It is shown red with a reason removed.
- **Every Elixir CI job runs in the pinned base image, and no job runs `apt-get`** (#365,
for #309). `.elixir` uses `CI_BASE_IMAGE`, pinned as `ci-base:<input hash>@sha256:<digest>`.
The per-job `apt-get update`/`install git` and `mix local.hex`/`local.rebar` are gone; the
memory and load diagnostics stay. `test/docs/ci_pipeline_test.exs` gates three things:
- no job runs `apt-get`;
- the pin is a digest, under a tag equal to the hash of `ELIXIR_IMAGE` and
`ci/base.Dockerfile`, so bumping either without rebuilding fails a test;
- every job rule names `$CI_PIPELINE_SOURCE`, since a bare `changes:` rule opened a
one-job MR pipeline that stood as !236's head pipeline.
Each is shown red against a bad fixture and against `main`'s pipeline.
- **A CI base image with `git`, Hex and Rebar baked in** (#364, for #309).
`ci/base.Dockerfile` builds it from `ELIXIR_IMAGE`, and the new `ci-base-image` job pushes
it to the project registry, only when the Dockerfile changes or when run by hand. Its tag is
a hash of its inputs, so an unchanged image builds nothing, and it reports the pushed digest.
No job uses it yet: #365 pins `.elixir` to that digest and removes the per-job `apt-get`,
which failed whole pipelines on a runner that cannot reach the Debian archive.
- **CI restores dependencies with depdep v0.10.0** (#363, for #349). It corrects a git
dependency's `origin` on restore, the second cause of `restored, but Mix would rebuild it`:
Mix compares the lock's URL with the restored checkout's `origin` as strings. Keys and the
schema are unchanged, so the store needs no refill. extla's own figure was already 0 under
v0.9.0; the fix is for peers restoring extla, whose objects are stored under both
`git@…` and `https://…` spellings.
- **surfex is pinned at `~> 0.6.1`, and the type-citation stopgap is gone** (#361, for
#357). 0.6.0 makes each public `@type` an item (surfex#137, filed from #351), so
`ExTLA.State.t()` in spec/04 resolves as `t:ExTLA.State.t/0`, and the `normalise` rewrite
`.surfex.exs` carried for it is removed. 0.6.1 counts an ExUnitProperties `property` as a
test (surfex#141, filed from #353), so the 11 tagged properties now declare `verifies`,
including generated_models_test's D-27 worker agreement. Nothing is recorded yet: relating
the type citation and adopting the properties' claims are part of the baseline (#354).
`PACKAGE_SURFACE.md` records the new requirement. extla has no `require:`, so 0.6's
upgrade step doesn't apply.
- **The six spec/04 claims no test verified now each have one** (#358, for #356). Each
claim held; none needed a code change:
- the keyword form `invariant :x, desc: "…", do: expr` (and likewise for
`action_property`, `terminal`, `temporal`) compiles to the same declarations and
model-checks to the same verdict as the block form;
- `ExTLA.Spec.DSL` defines no `spec` macro;
- `mix extla.check` declines liveness under `--workers 2` and under a `symmetry:`
declaration, and says why, where the same refutable property otherwise exits 1;
- `assert_spec` passes a refutable temporal property it was not asked to check, warns,
and flunks when `check_liveness: true`;
- a predicate cheap on most states and costly on a few is marked
`<-- varies by state`, while a uniform one is not. The test is deterministic by
construction and passed 50 of 50 repeats;
- `mix extla.explore`'s shortdoc names a saved counterexample rather than describing a
search.
Each test carries `@tag verifies:` for its section, so every section of spec/04 with
a claim now has a verifying test. Found while writing them: a bare capture (`&abs/1`,
`&+/2`) in a spec body is refused as an undeclared variable (#359).
- **spec/04 §§ Coverage → end say which tests verify them too** (#353, for #336). The other
17 sections were read the same way: Coverage, Profile, Trace, Parallel, `mix
extla.check` and its JSON schema, `mix extla.explore`, ExUnit Integration, and
Differential testing. With #352's half, spec/04 now carries 539 test → section claims
across 33 files, and every section with a claim has at least one, except the six claims
in #356 (two of them found here). The bare "Mix Integration" heading has no text of its
own to verify. Of the 18 suggested `implements` relations in range, five were retired
with a reason: each names a module only as context (an analogy, a contrast, deferred
work, an aside). surfex sees `test` but not ExUnitProperties' `property`, so the 26
properties' tags declare nothing to it yet (surfex#141); they are kept, because they
are correct.
- **spec/04 §§ Overview → Liveness say which tests verify them** (#352, for #336). Each of
the 18 sections up to Coverage and Vacuity was read against its tests. The ones that
show a section's claims carry `@tag verifies: "<section id>"`: 253 test → section
claims across 17 files, as a test's tag, a `describe`'s or a module's. Every section with
a claim has at least one, except four claims no test shows, now #356. Three sections need
none: the Architecture diagram and the State-space reduction introduction describe
rather than claim, and View abstraction is deferred past v1. Of the 12 suggested
`implements` relations in range, the Overview's four were retired in `.surfex/` with a
reason: it only lists Layer 2's components, each of which has its own section. Tags
change no test's behaviour, and no relation is recorded yet: the baseline is #354.
- **surfex's relation log is wired up for spec/04, not yet gating** (#351, for #336).
`.surfex.exs` points surfex at `spec/04-layer2-model-checker.md` with `adoption: :trust`,
and `.surfex/` holds the (still empty) log. `Surfex.ExUnitFormatter` records every test
result at its version; the full suite took 192 s with it, against 200–224 s before. The
`test`, `mutation` and `docs` jobs keep their evidence as artifacts under their own names,
and a new `relation-evidence` job checks the log against all three together. It is
`allow_failure` until spec/04 is tagged and baselined (#352–#354). `namespace: "ExTLA"` is
required, because surfex's default camelizes the app name to `Extla`. A type citation
(`ExTLA.State.t()`) is read as its module until surfex resolves types itself
(surfex#137). On current main, `mix surfex.suggest` proposes 30 `implements` and 2,466
`tests` relations. `CONTRIBUTING.md` is new and states the per-MR loop.
- **CI restores dependencies with depdep v0.9.0, and every one now restores** (#346, for
#342). Under v0.7.0 one dependency, `telemetry`, was restored and then rebuilt on every run
as "outdated", and never replaced because the store already held it. The object was fine:
its entries carried the build path of the project that pushed it, so it unpacked where this
project's Mix never looks (depdep#131, the mechanism behind depdep#110). v0.9.0 moves each
restored tree to this project's own build path. The pin's own pipeline read `pulled 7,
missing 0` with nothing rebuilt or compiled in every job. Keys are unchanged, so there was no
store refill. v0.8.0's `--explain-rebuilt` comes along for the next refusal worth reading.
- **`wrong_init_index` was killed only on a lucky seed** (#393, for #392). The one test that
caught it was a generated property, which fails only when the generator builds a spec
with two `init` blocks that is refuted from the second. Measured: it survived 10 seeds of
100, and failed the mutation job of pipeline 5315, whose change touched no code. No fixed
test read `init_index`, the field a replay starts from: `TestSpecs.TwoStarts` has two
starts and no property, so nothing asked it for a counterexample.
`test/ex_tla/second_start_replay_test.exs` now does, deterministically, with a fixture
refuted only from its second start:
- an invariant's and an action property's counterexamples start at the second start and
pass `Trace.validate/3`;
- every state of `TwoStarts` regenerates (`StateGraph.state_at/2`) to the state its id
names.
All three tests fail under the mutant, which is now gated on that file. The `:tests` gate
also runs its files with `--exclude property`. A kill that rests on generated input is
now a survivor the first time it is swept, not a red pipeline later.
- **The mutation sweep's `:suite` gate measured nothing** (#389, for #380). It ran the whole of
`mix test` in the sweep's workspace, which copies `lib`, `test` and the build but not
`README.md`, `guides/` or `spec/`. The suite failed there with no mutant applied, so its
three kills (`skips_symmetry_canonicalization`, `wrong_init_index`,
`param_universe_from_the_right`) were never measured. After #379, `--check` kept their
recorded outcomes and stayed green.
- **`:tests` replaces `:suite`:** each such mutant names the test files that catch it. These
were found by running the whole suite with each mutant applied: `symmetry_test`,
`generated_models_test` (one property, killed on ten seeds of ten), and `coverage_merge_test`
with the parallel checker's tests. The gate runs those files only.
- **`mix extla.mutants --check` now fails on `inconclusive (fails_unmutated)`.** A gate that
fails without the mutant is broken, not flaky. A failure that didn't reproduce, and a rerun
that timed out, are still tolerated.
- **A catalogue test checks the lists:** every `:tests` mutant must name existing test files,
and an empty list matches no gate rather than running the whole suite.
- **A parallel-profile test named the denominator rule #239 replaced** (#388, for #386).
`profile_parallel_test.exs` said `run_reductions` "is the coordinator's" and asserted `> 0`,
which passes under either rule, so nothing failed when #239 changed the rule.
- **What it checks now:** that the denominator sums every worker's batch, as spec/04 Under
`--workers` says. An 8-worker run's `run_reductions` is at least a 1-worker run's; measured,
it is about 2.4 times.
- **Proven to fail under the old rule:** with each worker's bracket zeroed, the coordinator
alone reads about 0.6 times, and the test fails.
- **A mutation kill has to be the mutant's doing** (#379, for #378). Any failing gate used to
count as a kill, so main pipeline 4744 recorded `weakens_a_type_domain`, the catalogue's
one expected survivor, as killed. A failing gate is now re-run twice over only the tests
that failed, once with the mutant and once without it. It counts as a kill only if the
failure comes back with the mutant and goes away without it. Otherwise the result is
`inconclusive`, with the reason. `--check` keeps the recorded outcome for an inconclusive
mutant rather than reporting PROGRESS or REGRESSION, and recording refuses one. The job log
now names the failing tests of every kill and prints the output of every other non-survival.
The likely cause of 4744 was in the workspace: it lacked `.surfex.exs`, so the evidence
formatter (#336) crashed in every gate, and depending on timing that made a passing run
exit 1. The workspace now copies it, and a test asserts that a passing gate there survives.
- **A function capture in a spec body compiles** (#369, for #359). `&abs/1`, `&+/2` or
`&member?/2` in any block was refused as "undeclared variable: abs", with advice to declare
`variable :abs`. The capture's name node has a variable's shape, and the rewriter resolved
it as one. A capture now names a function, even where a declared variable shares the name
(`variable :size` beside `&size/1`), and a capture of a function that doesn't exist is
still refused, by Elixir's compiler, naming it. `spec/02` §1 states the rule.
`test/ex_tla/spec/captures_test.exs` uses bare, operator, helper, qualified and `&(&1 …)`
captures in every block kind, including `let` and a `params:` generator, and model-checks
the result.
- **`ExTLA.Set.cross_many/1` no longer names a caller that does not exist, and docstrings
that name a caller are checked** (#347, for #324). Its docstring and `spec/01` justified
the empty product being `{{}}` as "the answer the DSL needs" for an action with no
parameters. Nothing in `lib/` calls it. The DSL binds parameters with
`ExTLA.ModelChecker.bindings/3`, a *dependent* product (each parameter's values may depend
on the state and on earlier parameters), which `cross_many/1`'s fixed list of sets cannot
express. The two are different operations, so the rationale now stands on its own: the
empty tuple is the identity of the product. `test/docs/caller_claims_test.exs` reads every
`lib/` `@doc` and `@moduledoc` from the AST. A backticked project function named in a
caller claim must exist, and in a function's doc a named caller (called from, used by)
must reach the documented function, directly or through its own module's helpers. Its
first run found `ExTLA.Profile`'s moduledoc naming `take_action/6` and
`enabled_bindings/3` as though they were in `ExTLA.ModelChecker.Safety`; they are in
`ExTLA.ModelChecker`, which the sentence now names. The gate also refuses a *qualified*
reference to a private function: ex_doc links it, and the docs job's
`--warnings-as-errors` refuses the link, which is how this MR's first pipeline failed. A
claim that names no function, like the old
"the DSL needs", is not refused, because `lib/` uses the same phrasing for concepts
("what Layer 3 needs"). Three more copies of the independent product (`record_set/1`,
`function_set/2`, `Symmetry.mappings/2`) are #350.
- **`ExTLA.Invariant.Test.valid_states/3` now says what a broad base generator costs**
(#348, for #344). It filters the base generator through the type invariant, and
`StreamData.filter/3` raises `FilterTooNarrowError` after 25 rejections in a row, but
nothing told a consumer that. Measured on a real type invariant over 2,000 seeds, 100-run
properties raised in none of the runs at about 50% acceptance, in 1 in 90 at about 30%,
and in 3 in 4 at about 15%. The 30% band is the dangerous one: it passes locally and goes
red on a rare seed. The docstring and `spec/03` §`valid_states` now say the base generator
should have the type's shape and be accepted at least about half the time, with a good and
a bad example, both held by a test. Another test reads the limit from the exception and
checks that the docstring and the spec state the number StreamData enforces. There is no
new `max_consecutive_failures:` option: raising the limit would move the failing band, not
remove it.
- **A property failed on one run in about 12,000, and a guard now makes generator filters say
why** (#343, for #341). `helpers_test.exs`'s out-of-domain property drew an index and then
filtered it with `m not in 1..length(s)`. A filter clause in `check all` rejects into the
generator before it, which raises `StreamData.FilterTooNarrowError` after ten rejections in
a row. With up to 6 of 21 draws rejected, that happened on 5 of 60,000 seeds, including CI's
796610 on v0.4.0's release MR. It had been there since #242 (2026-09-11), unseen because CI
draws a fresh seed per run. The property now generates the same out-of-domain values
directly: 0 failures in the same 60,000 seeds. The guess that StreamData's `integer/1`
shrinks its range at small sizes was wrong, since its documentation says the size is
ignored. `test/docs/property_filters_test.exs` reads `lib/`, `ledger/` and `test/` and
refuses any filter clause in `check all`/`gen all`, or any `StreamData.filter`, without a
`# filter: <reason>` above it. The one deliberate filter,
`ExTLA.Invariant.Test.valid_states/3`, now carries its reason.
63 commits since v0.4.0, merges included.
Tagged at 47304f6c2198.
