The formal relationship between an abstract specification and a concrete implementation.

A refinement mapping is a function from concrete states to abstract states such that the abstract behaviour obtained by mapping each concrete state satisfies the abstract spec. It is the mathematical content of implementation verification — but only when the steps are checked against the spec's actions, not merely the states against its invariants (see "What conformance checks" in guides/reference.md).

The three callbacks

abstract(concrete_state)            what the spec's variables mean here
abstract_action(message)            which spec action a message is meant to be
concrete_message(action, params)    the inverse: what message causes that action

abstract_action/1 is required rather than optional. Without a named action there is nothing to check the step against, and the layer degrades to invariant checking on a projection — which passes every implementation bug that reaches a legal-looking state by an illegal route. :unmapped is a positive claim that the message must not move the abstract state, and it is checked as one.

concrete_message/2 is optional. Without it an implementation can still be checked as it runs, but it cannot be driven from the spec, which forgoes ExTLA.Replay and most of what Layer 3 is for.

What validate!/3 establishes, and what it does not

A mapping is held to five rules. Three are decidable where validate!/3 runs and two are not, and saying which is which is the point — a validator that claims a check it cannot perform is worse than one that states its limits.

Decided at compile time:

• abstract_action/1 is total, established by probe: a term the implementation cannot have anticipated must come back :unmapped rather than raising inside a callback wrapper.
• concrete_message/2 round-trips, where it is defined and the constants are known.
• every spec action is named by some clause — but only where concrete_message/2 exists to enumerate them with. Elsewhere it is left to ExTLA.Coverage's account of what a run actually exercised, which is where "this action never happened" belongs.

That last rule has two halves, and they are established by different means. Whether concrete_message/2 has a clause for an action is a list comparison: use ExTLA.Refinement installs an @on_definition hook — the mechanism Layers 1 and 3 already use — that records the first argument of every clause, and the actions the spec declares are compared against that record. Whether the message a clause produces maps back is a probe, and needs a binding. So an action with no binding at compile time is still checked for having a clause, and only the round-trip half of the rule is deferred.

A clause whose first argument is a variable covers every action and is read that way. And concrete_message/2 is optional: a mapping that defines none is legal and reported as such, one that defines all passes, and one that defines some is the finding: the actions it leaves out can be checked as they happen but never driven.

Left to runtime, because there is no concrete state at compile time to map:

• abstract/1 returns exactly the spec's variables, and
• every value it returns is a permitted state term (02-dsl-semantics.md §6).

abstract!/3 checks both on every mapping. It is a Map.keys comparison and a ExTLA.State.validate!/1, cheaper than the invariants evaluated beside it.

Purity of abstract/1 is not checked: it is not decidable, and an impure mapping surfaces as a :diverged step instead. It is a documented obligation on the author.