The shared reachability walk: given a starting TypedTLAPlus.Expression, resolves every .var name _ (.module m) against m's declaration list and, for anything with a body (operator/function), recurses into that body too, transitively, memoized so a declaration referenced from multiple places is walked once. Every visited (module, name) pair, with what it resolved to, accumulates into a ReachabilityClosure returned to the caller.

Split out from WellFormedness/Restrictions.lean so Typed2Computable can reuse the same resolution/recursion/memoization machinery to collect "every constant/variable/operator/ function reachable from the algorithm," without inheriting Restrictions.lean's own error-throwing checks. walkReachable's visit parameter is the seam: Restrictions.lean supplies its checks through it; a caller that only wants the closure supplies a no-op. Checks run once per node via visit, in the same pre-order the walk visits nodes (visit, then recurse into children).

TypedPlusCal.Statement.walkReachable/.Algorithm.walkReachable below extend the same sharing to the statement-level traversal — which expression positions exist in a statement, and how they nest through Block/Branches. Two callbacks: visitStatement (a statement's own non-expression positions — Restrictions.lean's Ref channel-likeness checks on assign's LHS/receive's destination) and visitExpr (forwarded into Expression.walkReachable). Typed2Computable supplies no-ops for both, wanting only the ReachabilityClosure; Restrictions.lean supplies its real checks for both, and wraps its own StateT ReachabilityClosure at its own call site — Algorithm.walkReachable leaves .run vs .run' to the caller, same as Expression/Statement.walkReachable.

inductive ResolvedDecl : Type

What a name resolves to inside one module's declaration list, alongside the raw Decl itself (needed by callers that do more than classify it — Typed2Computable re-emits referenced constants/variables and translates referenced operator/function bodies). assume entries never resolve — falls through to none in Decl.resolve below, same as "not found".

• constant (decl : Decl) : ResolvedDecl
• variable (decl : Decl) : ResolvedDecl
• operatorOrFunction (decl : Decl) (body : TypedPlusCal.Expression) : ResolvedDecl

def Decl.resolve (name : String) : Decl → Option ResolvedDecl

Resolves name against one declaration d — some iff d is the constants/variables entry that declares name, or the operator/function definition named name.

Equations

• Decl.resolve name (Declaration.constants xs) = if (xs.any fun (x : String × TypedTLAPlus.Typ) => x.1 == name) = true then some (ResolvedDecl.constant (Declaration.constants xs)) else none
• Decl.resolve name (Declaration.variables xs) = if (xs.any fun (x : String × TypedTLAPlus.Typ) => x.1 == name) = true then some (ResolvedDecl.variable (Declaration.variables xs)) else none
• Decl.resolve name (Declaration.assume a) = none
• Decl.resolve name (Declaration.operator a f a_1 body) = if (f == name) = true then some (ResolvedDecl.operatorOrFunction (Declaration.operator a f a_1 body) body) else none
• Decl.resolve name (Declaration.function a f a_1 body) = if (f == name) = true then some (ResolvedDecl.operatorOrFunction (Declaration.function a f a_1 body) body) else none

def resolveInModule {m : Type → Type} [Monad m] [MonadForeignLookup m] (currentModule : String) (ownDecls : List Decl) (targetModule name : String) : m (Option ResolvedDecl)

Resolves name against targetModule's own declaration list — currentModule's own ownDecls (already in hand, no lookup) if targetModule is the module currently being walked, else lookupForeign targetModule's (WellFormedness/Monad.lean). none if targetModule can't be found at all (should be unreachable — a name only carries origin := .module m because m already type-checked it) or name isn't in its list (an ASSUME entry, or genuinely absent).

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev ReachabilityClosure : Type

Every (module, name) pair the walk has resolved so far, alongside what it resolved to.

Equations

• ReachabilityClosure = Std.HashMap (String × String) ResolvedDecl

partial def TypedTLAPlus.Expression.walkReachable {m : Type → Type} [Monad m] [MonadForeignLookup m] [MonadStateOf ReachabilityClosure m] (visit : List String → TypedPlusCal.Expression → m Unit) (currentModule : String) (ownDecls : List Decl) (path : List String) (e : TypedPlusCal.Expression) : m Unit

The shared walk. Visits e and everything structurally reachable from it — every opCall's function/arguments, every quantifier's domain/body, etc. — calling visit path once per node before recursing into its children (path, innermost first, grows only when the walk recurses into a resolved declaration's body — the breadcrumb Restrictions.lean's error messages report "reached via" through).

Whenever a node is .var _ (.module m name), resolves (m, name) and, the first time this pair is seen (ReachabilityClosure-memoized, guarding against looping on a self-recursive function — operators never self-recurse, per Elaborator/Declarations.lean — so only function bodies can cycle), records the resolution and, if it resolved to an operator/function, recurses into its body too (path extended by name). A constant/variable resolution is recorded but never recursed into. Resolutions after the first for an already-visited pair are no-ops for recursion — visit still runs on every node regardless, since some checks are per-reference, not per-declaration.

partial def TypedPlusCal.Statement.walkReachable {m : Type → Type} [Monad m] [MonadForeignLookup m] {b : Bool} [MonadStateOf ReachabilityClosure m] (visitStatement : {b : Bool} → Statement b → m Unit) (visitExpr : List String → Expression → m Unit) (currentModule : String) (ownDecls : List Decl) (s : Statement b) : m Unit

Visits every statement in s's tree — visitStatement once per statement, before recursing into substructure — and threads every expression position (print's e, assign's per-pair e, every Ref.args, …) through Expression.walkReachable via visitExpr, always with a fresh [] path (path only grows inside one expression's own walk, when it recurses into a resolved declaration's body).

send's/receive's channel-argument Ref (c) and any non-channel Ref position (assign's LHS, receive's destination r) are treated identically here — walking args, nothing else; Restrictions.lean's asymmetric channel-likeness check between the two lives entirely in its own visitStatement, which sees the raw Statement and can tell them apart.

partial: recursion isn't visibly decreasing to Lean through the mutual Block/Branches nesting.

def TypedPlusCal.Declarations.walkReachable {m : Type → Type} [Monad m] [MonadForeignLookup m] [MonadStateOf ReachabilityClosure m] (visitExpr : List String → Expression → m Unit) (currentModule : String) (ownDecls : List Decl) (d : Declarations) : m Unit

Walks every expression embedded in d — every variables entry's initializer, every channels/fifos entry's index-type expressions. Declarations has no further substructure to recurse into. Covering these positions is what keeps a CONSTANTS/VARIABLES entry referenced only from a process's own id/Declarations, and never from a statement body, from being reported as unreachable — and keeps a banned construct in such a position from going unchecked.

Equations

• One or more equations did not get rendered due to their size.

def TypedPlusCal.Algorithm.walkReachable {m : Type → Type} [Monad m] [MonadForeignLookup m] [MonadStateOf ReachabilityClosure m] (visitStatement : {b : Bool} → Statement b → m Unit) (visitExpr : List String → Expression → m Unit) (currentModule : String) (ownDecls : List Decl) (algo : Algorithm) : m Unit

Walks every expression reachable from algo — every statement (via Statement .walkReachable), every process's own id/mailbox index expressions, and both globalState's and every process's own localState's embedded expressions (Declarations.walkReachable above). Doesn't wrap its own ReachabilityClosure StateT layer: callers choose .run (keep the closure — Typed2Computable's use) or .run' (discard — Restrictions.lean's use), same choice Expression/Statement.walkReachable leave open.

Equations

• One or more equations did not get rendered due to their size.