Which spec variables each block reads and writes, computed at compile time.

This is the foundation of property-directed slicing: a run that checks only some properties need not distinguish states that differ outside those properties' cone of influence. That cone is derived from the read/write sets recorded here.

Why this has to happen in the macro

ExTLA.Spec.Block compiles an action body into guard and transition functions, so by the time the checker runs there is no AST left — actions are closures, pure functions of the pre-state and params (02-dsl-semantics.md §3). The dependency sets can only be derived while the quoted body is still in hand. ExTLA.Spec.Compiled already keeps variable_def.type_expr quoted for resolution at model-check time, so retaining compile-time structure is an established pattern here rather than a new one.

Widening is the default

A read set is :all unless every node in the expression is recognised. That ordering is deliberate and it is the whole soundness argument: an analysis that narrows by default and widens on the cases someone remembered is how an unsound optimisation ships. Here the narrowing has to earn its way in, node by node.

The one construct that can genuinely hide a variable read is a local macro: it expands after this walk, so a reference it introduces is invisible now. Remote calls cannot hide one — their arguments are already in this AST — and a local function cannot either, because a spec variable exists only as a binding inside a block and is not in scope in a function body. So the rule is narrow and precise: recognised operators and special forms are walked, remote calls are walked, and anything else widens.

What is not a variable

^constant is a constant, not state, and never enters a read set — a state cannot differ in a constant. let bindings are local names; a body's own intermediates are not state either, though the expressions they are bound to are still walked.