Statement/showable/process/algorithm checking: checkStatement/checkBlock/checkBranches/ checkPlusCalDeclarations/checkProcess/checkAlgorithm, turning a CorePlusCal.Algorithm (Option Typ) (CoreTLAPlus.Expression (Option Typ)) (α still the optional, user-written @type annotation) into a TypedPlusCal.Algorithm.

A few notable points:

• [Multicast]'s e1 premise is checked against Set(τ) for the channel's own declared domain τ: e1 is the set of recipients, and each is what indexes the channel.
• Algorithm-level variables (Algorithm.globalState.variables) are checked the same way as a process's own local variables (checkVariables below, shared by both).
• A with-bound variable's/variables entry's optional annotation is checked against when present, otherwise inferred from the initializer. A multicast recipient's is not consulted at all — see [Multicast] below.
• [Goto] performs no type check at all — label existence is the well-formedness pass's job.
• A receive/send's channel reference, and a with/variables entry's Ref-typed destination, are checked via inferRef below, not Elaborator/Expressions.lean's inferExpr/checkExpr: CorePlusCal.Ref is a distinct type from CoreTLAPlus.Expression, needing its own small synthesis judgment — a Γ-lookup on name followed by Elaborator/Expressions.lean's own indexInto once per bracket group.
• A channel/FIFO declaration's Γ-binding domain follows the same n = 1/n > 1 reconciliation as function definitions (Elaborator/Declarations.lean): m = 1 binds a channel's own Γ-type at plain Address → Channel(τ); m > 1 needs the tupled ⟨Address,...⟩ → Channel(τ) domain.

@[reducible, inline]

abbrev SrcRef : Type

The checker's actual PlusCal input: CorePlusCal.* at α := Option Typ (a with-bound variable's/variables entry's optional @type) and β := SrcExpr.

Equations

• SrcRef = CorePlusCal.Ref SrcExpr

@[reducible, inline]

abbrev SrcStatement (b : Bool) : Type

Equations

• SrcStatement b = CorePlusCal.Statement (Option TypedTLAPlus.Typ) SrcExpr b

@[reducible, inline]

abbrev SrcBlock (b : Bool) : Type

Equations

• SrcBlock b = CorePlusCal.Block (Option TypedTLAPlus.Typ) SrcExpr b

@[reducible, inline]

abbrev SrcBranches (b : Bool) : Type

Equations

• SrcBranches b = CorePlusCal.Branches (Option TypedTLAPlus.Typ) SrcExpr b

@[reducible, inline]

abbrev SrcDeclarations : Type

Equations

• SrcDeclarations = CorePlusCal.Declarations (Option TypedTLAPlus.Typ) SrcExpr

@[reducible, inline]

abbrev SrcProcess : Type

Equations

• SrcProcess = CorePlusCal.Process (Option TypedTLAPlus.Typ) SrcExpr

@[reducible, inline]

abbrev SrcAlgorithm : Type

Equations

• SrcAlgorithm = CorePlusCal.Algorithm (Option TypedTLAPlus.Typ) SrcExpr

@[reducible, inline]

abbrev SrcMulticast : Type

Equations

• SrcMulticast = CorePlusCal.Multicast (Option TypedTLAPlus.Typ) SrcExpr

partial def showable : TypedTLAPlus.Typ → Bool

The showable predicate, used by print: Int/Bool/Str/Address atomic; Function/Set/Seq/Tuple/Record recursively (a Function is showable when both its domain and range are). Operator/Channel/Const/rigid type variables, and anything containing them, are not showable. Pure and non-monadic — callers must resolve τ's metavariables first (instantiateMVars, at the point of use) so .mvar _ => false only fires on a genuinely unresolved metavariable, not one already pinned to something showable. partial: nested List recursion over Tuple/Record's fields isn't visibly structurally decreasing to Lean.

partial def sendable : TypedTLAPlus.Typ → Bool

The sendable predicate, used by a channel's own declared element type (checkChannelDecl): the same restriction as showable (a CONSTANT isn't sendable either — it gets substituted by the user only after code generation, and an unsendable instantiation would silently break this invariant once compiled). Identical in shape to showable but defined separately since the two restrictions only happen to coincide today, not the same rule reused. Same non-monadic, resolve-first contract as showable.

@[implicit_reducible]

def instInhabitedStatement_elaborator {m : Type → Type} [Monad m] {b : Bool} : Inhabited (m (TypedPlusCal.Statement b))

Needed for the partial defs below to type-check at all (an arbitrary m isn't otherwise known nonempty).

Equations

• instInhabitedStatement_elaborator = { default := pure Inhabited.default }

@[implicit_reducible]

def instInhabitedBlock_elaborator {m : Type → Type} [Monad m] {b : Bool} : Inhabited (m (TypedPlusCal.Block b))

Equations

• instInhabitedBlock_elaborator = { default := pure Inhabited.default }

@[implicit_reducible]

def instInhabitedBranches_elaborator {m : Type → Type} [Monad m] {b : Bool} : Inhabited (m (TypedPlusCal.Branches b))

Equations

• instInhabitedBranches_elaborator = { default := pure Inhabited.default }

def checkPlusCalDeclarations {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (decls : SrcDeclarations) : m (TypedPlusCal.Declarations × List (String × TypedTLAPlus.Typ))

Declarations checking, shared by both Algorithm.globalState and a Process's own localState: variables first, then channels/fifos, each stage's bindings in scope for the next.

Equations

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

partial def checkStatement {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] {b : Bool} (s : SrcStatement b) : m (TypedPlusCal.Statement b)

Γ|Ξ⊩S ok — a transform, not a pure ok-judgment: every embedded CoreTLAPlus.Expression/Ref becomes a checked TypedPlusCal.Expression/Ref, and receive additionally gains its Coercion.

partial: no structurally-decreasing measure across the mutual group visible to Lean (Block's begin : List (Statement _ _ false) field).

partial def checkBlock {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] {b : Bool} (blk : SrcBlock b) : m (TypedPlusCal.Block b)

Γ|Ξ⊩B ok for atomic blocks — check every non-terminal statement, then the terminal one.

partial def checkBranches {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] {b : Bool} : SrcBranches b → m (TypedPlusCal.Branches b)

either's own branch list, checked pointwise — no dedicated rule beyond [Either] reusing Γ|Ξ⊩B ok per branch.

def checkProcess {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (proc : SrcProcess) : m TypedPlusCal.Process

Γ|Ξ⊩ p∈S ⋆ x1=e1;...;xm=em ⋆ T1...Tn ok: S must be Set(Address), checked without self in scope; everything else about a process — mailbox, local variables, every thread — is checked with self:Address already in scope. mailbox's filter/index expressions are inferred, unconstrained, but still need self in scope (@mailbox: agt[self]; is the standard idiom).

process (p = e) checks e against Address directly, not Set(Address) (dispatches on proc.«=|∈» rather than constructing a singleton set {e} and checking that).

Equations

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

def checkAlgorithm {m : Type → Type} [Monad m] [MonadElaborator m] [MonadPendingBounds m] (algo : SrcAlgorithm) : m TypedPlusCal.Algorithm

Γ|Ξ⊩ fifos c1:τ1,...,cm:τm; P1∥...∥Pn ok: every channel declaration checked (also covers globalState.variables), then every process checked against Γ extended by those bindings. Those bindings stay scoped to the algorithm itself — PlusCal declarations don't leak into the surrounding TLA⁺ module's own Γ.

Equations

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