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

Layer 1: invariants and properties on a running OTP process, checked at every transition.

    defmodule Account do
      use GenServer
      use ExTLA.Invariant

      invariant :never_negative, desc: "an account may not go below zero" do
        state.balance >= 0
      end

      action_property :no_free_money do
        new.balance <= old.balance or new.deposits > old.deposits
      end

      precondition {:withdraw, amount} do
        amount > 0
      end
    end

`state` is bound in an `invariant`, `old` and `new` in an `action_property`, and in a
`precondition` or `postcondition` the pattern's own bindings are in scope alongside
them. Nothing is passed in explicitly, because a property is a statement about the
process rather than a function of arguments.

## `defoverridable` and `super`, not renaming

The `@before_compile` hook wraps each callback the module defines by marking it
overridable and defining a new one that calls `super`, rather than renaming the
original. Every real GenServer has several `handle_call/3` clauses with guards; renaming
would have to reproduce every clause head and its guards exactly, and any mistake
silently changes dispatch. `super` keeps the original clauses intact and dispatches to
them with their own pattern matching.

`use ExTLA.Invariant` goes directly **after** `use GenServer` and **before** the
callbacks, and the order is load-bearing rather than stylistic. Only the callbacks the
module's own author writes are wrapped, and they are identified with `@on_definition`,
which sees a definition only after it is installed. That is what keeps the wrapper
off the default `handle_call/3`, `handle_cast/2` and `handle_info/2` that `use
GenServer` injects — `Module.defines?/2` cannot tell those from the author's, calling
`super` on them is deprecated, and wrapping a default that exists to stop the server
with a `:bad_call` is checking a transition nobody wrote.

**`init/1` is the exception, and it needs a second guard.** GenServer injects it
from its own `@before_compile`, which runs *after* the hook is installed rather than
before — so `@on_definition` does see it, and `{:init, 1}` lands in the wrapped set for a
module whose author wrote no `init/1`. By then GenServer's `defoverridable init: 1` has
moved it out of the definitions table, and `Module.make_overridable/2` refuses:

    ** (ArgumentError) cannot make function init/1 overridable because it was not defined

naming neither this library nor the cause — for a module as plain as the example at the
top of this moduledoc. So the wrapper is emitted only for a callback still in the
definitions table when `__before_compile__/1` runs — which is precisely what
`make_overridable/2` requires, asked as a question rather than assumed.

## `:disabled` emits nothing

When `ExTLA.Config.mode/0` resolves to `:disabled` where the module compiles, the hook
emits no wrapper and no `defoverridable`, and the module compiles exactly as written.
That is what "zero production cost" has to mean: not cheap emitted code, but none. It is
also why the mode is a `compile_env` macro — a runtime lookup would leave an
`Application.get_env/2` call and a branch on every callback, which alone would exceed the
budget the whole layer is meant to fit in.

## Cost is decided at compile time wherever it can be

`callbacks:` restricts an invariant to particular callbacks, and the restriction is
resolved when the wrapper is generated. A hot callback in a module with nine invariants
emits a call naming the two that apply, rather than nine names and a filter. Where a
callback ends up with nothing to check, no call is emitted for it at all.

`enabled: false` is evaluated at compile time and emits nothing anywhere, for a check too
costly to run outside a particular environment.

# `action_property`
*macro* 

A property of a transition. `old` and `new` are bound; same options as `invariant/3`.

# `invariant`
*macro* 

A state invariant, checked after every transition.

`state` is bound in the block. Options: `desc:` for the violation message, `enabled:`
(compile time — false emits nothing), and `callbacks:` to restrict it to some of them.

# `postcondition`
*macro* 

A condition checked after the matching callback returns. `old`, `new` and the pattern's
bindings are in scope.

# `precondition`
*macro* 

A condition checked before the matching callback runs.

`pattern` is matched against the incoming message and its bindings are in scope in the
block, alongside `state`. A message the pattern does not match has nothing to say about
it and passes — which is a different thing from a predicate that returned false, and the
two are reported differently.

---

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