# `ExTLA.Refinement`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/refinement.ex#L1)

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.

# `abstract`

```elixir
@callback abstract(concrete_state :: map()) :: ExTLA.State.t()
```

Concrete state -> abstract state. Must be pure.

# `abstract_action`

```elixir
@callback abstract_action(message :: term()) :: {atom(), map()} | :unmapped
```

Concrete message -> the spec action it is meant to be, or `:unmapped`.

# `concrete_message`
*optional* 

```elixir
@callback concrete_message(action :: atom(), params :: map()) :: term()
```

Abstract action and params -> a concrete message that should cause it.

# `abstract!`

Map a concrete state, checking the two rules that need a state to check.

The keys must be exactly the spec's variables: a missing one leaves the abstract state
short of a variable every predicate reads, and an extra one is a key the spec never
declared, which would make the state unequal to anything an action produces and turn
every step into a `:diverged`. Both are named here rather than diagnosed three frames
later.

# `validate!`

Verify that a refinement mapping is well-formed against a spec.

Returns the rules it could not decide, so a caller can say so rather than imply
everything was checked. Raises `ExTLA.Refinement.Error` on anything it can decide and
finds wrong.

---

*Consult [api-reference.md](api-reference.md) for complete listing*