# `ExTLA.Invariant.Runtime` [πŸ”—](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/invariant/runtime.ex#L1) The engine behind Layer 1's callback wrappers. Not called directly. Everything here is reached from code `ExTLA.Invariant`'s `@before_compile` emitted into the instrumented module, and the division of labour between the two is deliberate: **anything decidable at compile time is decided there.** The `callbacks:` option is resolved when the wrapper is generated, so a hot callback checking two of a module's nine invariants calls this with two names rather than nine and a filter. ## Telemetry `[:extla, :invariant, :violated]` and its three siblings fire whenever one does, if `:telemetry` is available β€” it is an optional dependency, and whether it was there is decided when ExTLA compiles rather than on every check. Success events are opt-in (`config :extla, telemetry: :verbose`) and **unemitted** otherwise, because `:telemetry.execute/3` costs about a microsecond even with no handlers attached and a single transition can fire four of them. Violations are rare and worth their cost; successes are the hot path. "Unemitted" is why each check has two arities. The wrapper calls the three-argument form unless the module compiled under `:verbose`, and that form contains no timing and no success event to skip β€” not a branch that declines to fire one. # `check_action_properties!` Check the named action properties over a transition. # `check_action_properties!` The same, under `:verbose`. # `check_agent_state!` Check the invariants of a state an `Agent` was read at, and return it. A read is a stuttering step: nothing moved, so there is no action property to check, but the invariants must still hold β€” the same reason a GenServer callback that returns its state unchanged is still checked. # `check_agent_step!` Check a transition that no wrapper produced: an `Agent` update. An `Agent`'s transitions are functions its *callers* pass in, so there is no callback to wrap and no compile-time place to resolve `callbacks:` β€” which is why this takes every declared name and why `callbacks:` is documented as meaningless for an `Agent` (Β§03 Β§Supported OTP Behaviors). Returns the new state, so it can stand in the middle of the `Agent.update/3` function it is called from. # `check_initial_invariants!` Check the named invariants against the state an `init/1` produced, if it produced one. The tag test lives here rather than in the emitted wrapper for a reason worth recording: inside a particular module, `super(arg)` has a known return type, so a `case` on `initial_state/1`'s tag has a clause the compiler can prove unreachable β€” and Elixir's type system says so, as a warning, in the user's module, about code the user did not write. Behind a function taking `term()` there is nothing to prove. # `check_initial_invariants!` The same, under `:verbose`. # `check_invariants!` Check the named invariants against a state. The names come from the wrapper, already filtered by `callbacks:`. # `check_invariants!` The same, timing each check and emitting a `:checked` event. Called only from a module compiled under `config :extla, telemetry: :verbose`. # `check_postconditions!` Check every postcondition whose pattern matches `message`. # `check_postconditions!` The same, under `:verbose`. A `:no_match` fires nothing, for the reason on `check_preconditions!/5`. # `check_preconditions!` Check every precondition whose pattern matches `message`. A message no pattern matches has no preconditions and passes β€” `:no_match` is the generated clause's way of saying "this declaration is not about this message", which is a different thing from a predicate that returned false. # `check_preconditions!` The same, timing each check that RAN and emitting a `:checked` event. Called only from a module compiled under `config :extla, telemetry: :verbose`. A `:no_match` fires nothing. The generated clause answers `:no_match` without evaluating the predicate β€” the declaration is not about this message β€” so an event saying a check happened would be a measurement of a check that did not occur, and its `duration` would be the cost of a pattern match reported as the cost of a precondition. # `extract_state` The post-state carried by a callback's return value. `pre_state` is the fallback because not every return carries one: `{:stop, reason, reply, state}` does, a bare `{:stop, reason}` from `handle_info` does not, and `:ignore` from `init/1` does not. Treating those as stuttering is right β€” nothing moved β€” and it keeps the wrapper from having to know which callback it is wrapping. # `extract_statem_state` The post-state carried by a `:gen_statem` callback's return value. A state machine's state is the `{state_name, data}` pair, so `pre` is both the fallback and the source of the name a `:keep_state` return leaves alone. This cannot be more clauses on `extract_state/2`: `{:stop, reason, new_data}` is a `:gen_statem` return carrying DATA, and the identically shaped `{:stop, reason, state}` is a GenServer return carrying the whole state. One function cannot answer both. `:gen_statem`'s `:state_functions` callback mode is not instrumented β€” its transitions live in functions named after the states, which `@on_definition` cannot recognise. Β§03 specifies `handle_event/4`, which is the `:handle_event_function` mode. # `initial_state` The first state an `init/1` produced, or `:none`. `:ignore` and a bare `{:stop, reason}` are refusals to start: there is no first state, and an invariant checked against its absence would report a violation of a predicate that was never given anything to be about. The `init/1` wrapper checks nothing in that case β€” which is why this returns a tag rather than a state and a fallback. # `initial_statem_state` The same for a `:gen_statem`, whose `init/1` returns `{:ok, state_name, data}`. A module is read as a state machine when it defines `handle_event/4`. Without this the shared `initial_state/1` would take `{:ok, :red, data}` for `{:ok, state, extra}` and check the invariants against the state NAME β€” which is not the state, and which a declaration written as `{name, data} = state` would refuse with a `MatchError` naming neither the invariant nor the reason. --- *Consult [api-reference.md](api-reference.md) for complete listing*