Pure structural/type-shape checks over a TypedPlusCal.Algorithm's declarations, no expression-walking or cross-module lookup needed:

• No variables entry (algorithm- or process-level) may have a Channel-shaped type — declare a channel via channels/fifos instead.
• A process's own localState.channels/.fifos must be empty — defense-in-depth; the parser already guarantees this, but nothing in CorePlusCal's/TypedPlusCal's own type enforces it structurally.
• The algorithm's own globalState.variables must be empty — no shared mutable state across processes. globalState.channels/.fifos and every Process.localState.variables are untouched by this.

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

Runs all three checks over a whole algorithm. The empty-globalState.variables check runs before the channel-shaped-entry check on globalState: every algorithm-level variables entry is already banned regardless of its type, so checking channel-shapedness first would report the misleading "declare it via channels/fifos instead" when the real problem is that no variables keyword is allowed there at all. The channel-shapedness check still runs afterward, but is a no-op there by construction.

Equations

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