Content versions for spec items and for a spec as a whole.
A verification result, and a refinement mapping, are claims about a specific version of a
spec. ExTLA.Refinement.abstract/1 is written against a set of spec variables; rename one
or change an action's post-state and ExTLA.Refinement.abstract_action/1 still compiles and
still returns an action name. The mapping is now wrong, and the only symptom is :diverged
at runtime, on a path that may not be exercised for months. A content version turns that
into a compile error.
The algorithm
Strip all AST metadata, Macro.to_string, sha256, first 8 hex. It ships with ExTLA
rather than coming from a dev-only dependency because the check it serves runs at the
consumer's compile: use ExTLA.GenServer, spec_version: … is written in the consumer's code,
so the algorithm must be available wherever that code compiles.
Metadata stripping is the point
A version is a function of an item's STRUCTURE, not its position. A blank line, a comment or reindenting above an action leaves its version alone; changing its body moves it. Without that, an edit near the top of a file would restamp everything below it and every stamp in the file would go stale at once — which teaches authors to restamp without reading, defeating the mechanism.
Summary
Functions
The declarations that carry no verdict but are part of the module version.
The content version of a quoted node or a source binary: 8 lowercase hex characters.
Every versionable item module declares, or %{} when its source is not on disk.
The kinds of item that carry a version of their own, each with a verdict of its own.
The version of module as a whole: 8 hex over every declaration it makes.
The version of module as declared in source, or nil when source does not define it.
Every versionable item declared anywhere in source.
Every versionable item module declares within source.
Types
Functions
The declarations that carry no verdict but are part of the module version.
Together with kinds/0, every declaration form the DSL has. A declaration form in neither
list would leave the module version blind to edits of it.
The content version of a quoted node or a source binary: 8 lowercase hex characters.
Every versionable item module declares, or %{} when its source is not on disk.
An absent source means "cannot version this", a different fact from "this has no version": a spec that arrived inside a released package has a version nobody here can compute, and callers render that differently from an item with none.
The kinds of item that carry a version of their own, each with a verdict of its own.
The version of module as a whole: 8 hex over every declaration it makes.
This is what a refinement mapping stamps. A mapping is written against the spec's variables and actions together, so the question it must answer is "has anything I depended on moved", not "has this one action moved" — and a per-item stamp on a mapping would be a list nobody maintains.
Every declaration, not only the items
variable, constant, init and fairness carry no verdict of their own, but they are in.
A stamp does not name a verdict; it names the specification somebody re-read a mapping
against. Changing an init value, a constant's default or a variable's type: changes the
reachable states a mapping must handle, so each moves the version — otherwise a mapping
would stay fresh across a new variable its abstract/1 cannot produce.
fairness changes liveness verdicts and nothing a mapping reads, but the version is one
number naming one specification, and a spec under strong fairness admits a different set of
behaviours from the same spec under weak. Leaving it out would need a second,
"liveness-relevant" version beside the "mapping-relevant" one.
What is not in: @moduledoc, @doc, use ExTLA.Spec, and any ordinary def in the
module. A helper function called from an action body would change meaning without moving
the version; hashing the whole module body instead would restamp every mapping on a
documentation edit, which teaches authors to restamp without reading.
Derived from declaration hashes rather than the file's bytes, so it inherits their
position-insensitivity: reformatting a spec does not invalidate every mapping written against
it. Returns nil when the spec's source is not on disk.
The version of module as declared in source, or nil when source does not define it.
mix extla.stamp reads specs from disk by path rather than through the loaded module; it
uses this function, so the compile-time check and the stamp task always agree about a spec's
version.
Every versionable item declared anywhere in source.
Every versionable item module declares within source.
Scoped to that module's own defmodule, NOT the whole file. One file may hold several specs,
and a file-wide scan would give them the same version, so editing one would mark every
mapping stamped against the other stale. A stamp going stale for something that did not
change is the same "cries wolf" failure position-insensitivity exists to prevent, arriving
by a different route.