Well-scopedness, the executable check over TypedPlusCal.Algorithm (run by the driver): every name is fresh in the scope it's declared in — no duplicate names within one flat declaration list, and no name shadowing an already-in-scope one from an enclosing scope. Scope classes: global (Algorithm.globalState), process-local (Process.localState), and block-local (with's own binder) — "channel" isn't a separate namespace from "global"/ "process-local" here (variables/channels/fifos already coexist in one flat scope per Declarations value), so it's folded into whichever of those two applies.

Process names are checked here too, as a flat scope of their own — they clash with each other and with nothing else. See Algorithm.checkWellScoped for why they must be distinct at all.

This is only the "no duplicate names / no shadowing" half — "every reference resolves to a declared name" is redundant with type checking's own success and isn't re-derived here.

The Prop-side counterpart for each later PlusCal stage (WellFormedness.WellScoped. CorePlusCal, .GuardedPlusCal) lives in its own file, modeled on the same scope-class shape but not executed and not invoked by anything here.

partial def TypedPlusCal.Statement.checkWellScoped {m : Type → Type} [Monad m] [MonadDiagnostic WellFormednessWarning WellFormednessError m] {b : Bool} (inScope : List String) (s : Statement b) : m Unit

Walks every with binder reachable from s, checking it against inScope and extending it for the sub-block. No other statement introduces a PlusCal-visible name.

Keeps its own recursion rather than using ElaboratedPlusCal.Statement.forEachNode — inScope grows at each with and only for that binder's own sub-block, so the check and the recursion can't be separated the way Labelling.lean's can.

def TypedPlusCal.Algorithm.checkWellScoped {m : Type → Type} [Monad m] [MonadDiagnostic WellFormednessWarning WellFormednessError m] (algo : Algorithm) : m Unit

Well-scopedness over a whole algorithm: the processes distinct among themselves; global declarations fresh among themselves; each process's own local declarations fresh among themselves and not shadowing a global one; every with binder inside a process's threads fresh against global ++ that process's own locals ++ whatever outer withs it's nested in.

Process names are their own flat scope, not part of any declaration scope: a process and a variable may share a name and nothing is ambiguous. What makes them have to be distinct is dispatch rather than scoping — a process instance is ⟨process name, self⟩, and both languages' semantics resolve one by processes.find? (·.name == name), the first process carrying it. Two processes sharing a name would silently give every instance of the second the first's code and labels, while the initial state still contributed instances from both. Checked first, before any declaration is looked at, since it is a property of the algorithm rather than of a scope inside it.

Equations

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