Well-labelledness: every goto targets a label its process actually defines, or the reserved "Done"; "Done" itself is never a real, user-defined label.

Assignment-conflict checking is not duplicated here — it already runs in Desugarer/PlusCal.lean's CorePlusCal.Algorithm.checkAssignConflicts.

def TypedPlusCal.Process.labels {m : Type → Type} [Monad m] [MonadDiagnostic WellFormednessWarning WellFormednessError m] (p : Process) : m (List (String × SourceSpan))

Collect every label a process defines across all its threads (Process.threads, the label of every atomic block), paired with that block's own terminal-statement position — needed both to check goto targets and, concatenated across every process (checkLabelling below), to check for a repeated label. Rejects a literal "Done" entry along the way — "Done" is a reserved fallthrough target, never itself a real label. No better position exists for a redefinedDone error than the labelled block's own terminal statement: labels are bare strings paired with a block, not positioned nodes in their own right.

Equations

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

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

Checks one goto l, within its own process, against that process's own labels ∪ {"Done"} — a goto can only ever reach a label in its own process's control flow (Process.codeTable is built per process), even though labels are drawn from one algorithm-wide namespace. A per-node check with no context of its own beyond labels, so it does no recursing — ElaboratedPlusCal.Statement.forEachNode (Core/TypedPlusCal/Syntax.lean) supplies that. Every non-goto statement is vacuously fine.

Equations

• One or more equations did not get rendered due to their size.
• TypedPlusCal.Statement.checkGotoTarget labels s✝ = pure ()

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

Well-labelledness over a whole algorithm: labels form one flat namespace across every process, checked for uniqueness once, algorithm-wide; then, per process, every goto in every one of its threads must target one of that same process's own labels or "Done".

Equations

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