Check the classified statements of an action body and return the assignments, in source order, having rejected a variable assigned twice or not declared.

Bind each param to a local of the same name, so the block can read from where params: [from: ^accounts] was declared.

The binding is marked generated: true — including on the variable itself, not only on the match — because a guard that does not mention every param is perfectly normal and should not warn.

Wrap a compiled predicate body so a non-boolean result is refused at run time.

Elixir's and/or return their last operand, so n >= 0 and status evaluates to status. Tested for truthiness, that predicate would count as holding whenever status was anything but nil or false — a run in which it never took the value the author had in mind would report :ok. Wrapping the body once, here, gives the checker, trace replay and coverage the same refusal without each of them re-deriving it; see ExTLA.Spec.PredicateError.

Reject a binder that shadows a declared variable or constant.

§1.3 says a let may shadow nothing, and the rule is about what a bare name means, not about let: any binder inside a spec block that captured a declared name would make the same bare name mean two things in one spec. binder names the construct for the message — "let" or "the quantifier".

Public because the temporal quantifier needs the same rule. Without it, Enum.all?(^procs, fn p -> … end) with variable :p declared would resolve the body's p to the state variable — the rewriter consults declared variables before bound names — so every instance would read state.p, the bound value would never be used, and the formula would report a verdict about the wrong thing.

Classify one statement of an init or action body.

Prepare a predicate block — invariant, terminal, action_property.

let becomes an ordinary match, and an assignment to a declared variable is rejected: §1.2 permits assignment only in init and action, where it means "the post-state". In a predicate there is no post-state for it to mean.

The guard: the conjunction of the block's requires, evaluated on the pre-state with params bound.

lets are interleaved in source order rather than hoisted, so a require may guard the let that follows it — require Map.has_key?(f, k) before let v = f[k] has to actually protect it, which it only does if and short-circuits over the binding.

The initial state: every declared variable, assigned exactly once.

An init that leaves a variable out would produce a partial state, and the omission would surface much later as a KeyError from whichever action first reads it — a long way from the declaration that caused it.

The near-miss expression of an invariant, or nil when there is none.

A near miss is a state in which the invariant held only through its non-trivial branch: the left disjunct of a top-level or was false, so the right one had to carry it. An invariant with no near misses over a whole run was never pressed against, and is indistinguishable from true.

Only the top-level or shape is derived here. For an invariant without one, nil means not measured — which the coverage report must render differently from zero, since zero is the finding and "not measured" is not. The atomic-bound shape that would measure a bare count <= max is not derived:

# An implication gets a probe: the negated left disjunct.
iex> ExTLA.Spec.Block.near_miss(quote(do: a or b)) |> Macro.to_string()
"not a"

# A bare comparison does not, and `nil` means NOT MEASURED.
iex> ExTLA.Spec.Block.near_miss(quote(do: count <= max))
nil

Reject = on a declared variable, where there is no post-state for it to mean.

02-dsl-semantics.md §1.2 permits assignment only in init and action. In a predicate or a temporal formula there is no post-state, so = on a declared variable is almost always a mistyped ==.

Public because two paths need the same rule: predicate blocks reach it through desugar_predicate!/2, and a temporal block, which is parsed by ExTLA.Spec.Temporal.parse!/2 and never desugared, calls it directly.

Without it a temporal built from an assignment would compile, and that is the worst shape a missing check can have. An invariant that never fires is visible in the coverage report; a temporal formula built from an assignment is not refutable, so the run would report that the property holds — a green verdict for a property that checked nothing.

Returns :ok, or raises ExTLA.Spec.CompileError. Anything that is not an assignment to a declared variable passes through.

Scope

The whole expression is walked, not just its top-level statements. In a temporal the top level is nearly always always, eventually or ~>, so a statement-level check would let always(x = 1) through. A nested = is legal Elixir, but the check fires only for = on a declared variable, which §1.2 forbids everywhere outside init/action, nested or not, so there is no legitimate case the walk could reject.

Split a block into its top-level statements.

The transition: the post-state, as one merge of the assigned variables onto the pre-state. A variable not assigned is untouched, which is UNCHANGED.