The well-formedness pass's diagnostics: one named error variant per violation, plus the one non-fatal finding — a @mailbox nothing receives on, which is dropped rather than rejected.

inductive WellFormednessError : Type

The well-formedness pass's errors.

• unknownLabel (pos : SourceSpan) (label : String) : WellFormednessError

  A goto targets a label that doesn't exist anywhere in its process ("Done" always counts as existing).

• redefinedDone (pos : SourceSpan) : WellFormednessError

  "Done" used as a real, user-defined label.

• duplicateName (pos : SourceSpan) (name : String) : WellFormednessError

  A name is declared more than once in a scope where every name must be fresh.

• shadowedName (pos : SourceSpan) (name : String) : WellFormednessError

  A name shadows an already-in-scope name, in a scope where shadowing isn't allowed.

• channelInExpression (pos : SourceSpan) (τ : TypedTLAPlus.Typ) : WellFormednessError

  A channel-shaped value appears inside an ordinary expression — only send/receive's channel argument and multicast's target may reference one. No name field: the offending subexpression need not be a bare variable (e.g. IF b THEN ch1 ELSE ch2), so τ (the Channel-shaped type actually found) is the only thing always available, matching TCError.notAChannelType's own shape.

• channelTypedVariable (pos : SourceSpan) (name : String) : WellFormednessError

  A variables/with-declared name (algorithm-level, process-level, or with-bound) has a Channel-shaped type — the channels/fifos forms are the only legitimate way to declare one.

• nonEmptyLocalChannels (pos : SourceSpan) (process : String) : WellFormednessError

  A process's own localState.channels/.fifos isn't empty — defense-in-depth; the parser already guarantees this today.

• globalPlusCalVariable (pos : SourceSpan) (name : String) : WellFormednessError

  The PlusCal algorithm itself declares algorithm-level variables (shared mutable state across all processes) — only fifos is allowed at that level.

• globalTLAPlusVariable (pos : SourceSpan) (name definedIn : String) : WellFormednessError

  A reference inside the algorithm resolves to a TLA⁺ module-level VARIABLE — definedIn names the module that actually declared it (own or, via EXTENDS, a dependency's).

• bareTemporalOrAction (pos : SourceSpan) (op : String) (path : List String) : WellFormednessError

  A temporal formula or action operator ([], <>, ENABLED, UNCHANGED, ', ^+, ^*, ^#) appears somewhere the algorithm's expressions reach — directly in a statement (path := []) or transitively, through an operator/function call chain (path the sequence of operator names traversed to get there, innermost first).

• unboundedQuantifier (pos : SourceSpan) (path : List String) : WellFormednessError

  An unbounded quantifier (\A x : P/\E x : P/CHOOSE x : P, no domain) appears somewhere the algorithm's expressions reach — same direct-vs-transitive path shape as bareTemporalOrAction.

• receiveChannelMismatch (pos : SourceSpan) (process expected found : String) (indicesDiffer : Bool) : WellFormednessError

  A process receives from a channel other than the one it already listens on — its declared @mailbox if it has one, otherwise the channel its first receive names. expected/found are the two channels' names; they can be equal and the channels still differ, when the index expressions do (agt[self] vs agt[other]), which indicesDiffer distinguishes.

• mailboxNotIndexedBySelf (pos : SourceSpan) (process channel : String) : WellFormednessError

  A ∈-shaped process (a process set) receives from a channel whose index path does not mention self, so every instance of the set would drain the same FIFO.

• receiveWithoutMailbox (pos : SourceSpan) (process channel : String) : WellFormednessError

  A process receives without declaring a @mailbox. The channel a process listens on is the one thing Guarded2Network's single inbox per instance is indexed by, so it has to be written down rather than inferred from whichever receive the walk happens to reach first.

• duplicateProcessName (pos : SourceSpan) (name : String) : WellFormednessError

  Two processes of one algorithm carry the same name. Separate from duplicateName, which is about a scope: process names are not in any declaration scope — a process and a variable may share a name — but they are what the semantics dispatches an instance on, so they must be distinct among themselves.

• duplicateLabel (pos : SourceSpan) (label : String) : WellFormednessError

  Two blocks of one algorithm carry the same label. Separate from duplicateName: labels are their own namespace (WellFormedness/Labelling.lean's Process.labels), not a declaration scope, and — matching the original PlusCal-to-TLA⁺ translator, whose labels each become their own top-level TLA⁺ definition — that namespace spans the whole algorithm, not just one process. Within one process it is additionally an operational hazard: Process.codeTable treats a label as denoting the union of every block carrying it, so a duplicate isn't rejected there — it silently becomes a non-deterministic choice between the blocks, which is never what the source program meant when it wrote a goto to that name.

def instReprWellFormednessError.repr : WellFormednessError → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprWellFormednessError : Repr WellFormednessError

Equations

• instReprWellFormednessError = { reprPrec := instReprWellFormednessError.repr }

@[implicit_reducible]

instance instInhabitedWellFormednessError : Inhabited WellFormednessError

Equations

• instInhabitedWellFormednessError = { default := instInhabitedWellFormednessError.default }

def instBEqWellFormednessError.beq : WellFormednessError → WellFormednessError → Bool

Equations

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

@[implicit_reducible]

instance instBEqWellFormednessError : BEq WellFormednessError

Equations

• instBEqWellFormednessError = { beq := instBEqWellFormednessError.beq }

@[implicit_reducible]

instance instCompilerDiagnosticWellFormednessErrorString : CompilerDiagnostic WellFormednessError String

Equations

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

inductive WellFormednessWarning : Type

The well-formedness pass's warnings.

• unusedMailbox (pos : SourceSpan) (process channel : String) : WellFormednessWarning

  A process declares a @mailbox and contains no receive. The declaration is dropped, so that a .some mailbox means exactly "this process receives, on this channel".

@[implicit_reducible]

instance instReprWellFormednessWarning : Repr WellFormednessWarning

Equations

• instReprWellFormednessWarning = { reprPrec := instReprWellFormednessWarning.repr }

def instReprWellFormednessWarning.repr : WellFormednessWarning → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instInhabitedWellFormednessWarning : Inhabited WellFormednessWarning

Equations

• instInhabitedWellFormednessWarning = { default := instInhabitedWellFormednessWarning.default }

def instBEqWellFormednessWarning.beq : WellFormednessWarning → WellFormednessWarning → Bool

Equations

• instBEqWellFormednessWarning.beq (WellFormednessWarning.unusedMailbox a a_1 a_2) (WellFormednessWarning.unusedMailbox b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• instBEqWellFormednessWarning.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instBEqWellFormednessWarning : BEq WellFormednessWarning

Equations

• instBEqWellFormednessWarning = { beq := instBEqWellFormednessWarning.beq }

def WellFormednessWarning.name : WellFormednessWarning → String

The -W<name> a given warning is filtered under.

Equations

• (WellFormednessWarning.unusedMailbox a a_1 a_2).name = Diagnostics.unusedMailbox.warningName

@[implicit_reducible]

instance instCompilerDiagnosticWellFormednessWarningString : CompilerDiagnostic WellFormednessWarning String

Equations

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