The output of Computable2Guarded: every guard (await/receive/with) sits at the very start of its atomic branch. Reuses ElaboratedPlusCal.Ref/.Multicast rather than redefining them — Computable2Guarded's Ref field-access fix (Core/TypedPlusCal/Syntax.lean) flows through automatically. Unlike ElaboratedPlusCal, Statement here is genuinely flat: by this stage every if/while/either has already been rewritten away into AtomicBranch's precondition/action split (𝒞_cflow/𝒞_flat/𝒞_reord), so no constructor embeds a nested Block/Branches the way CorePlusCal.Statement.if/.while/.either do — no mutual, partial, or position tracking is needed anywhere in this file (ElaboratedPlusCal carries none either, see Typed2Computable/PlusCal.lean's module doc).

Block, unlike every other type here, is generic over an arbitrary index family α : Bool → Type, not (Typ Expr : Type), since it's purely structural and doesn't reference Typ/Expr at all. Block (Statement Typ Expr true) false/Block (Statement Typ Expr false) true both instantiate it.

Pinned at ComputableTLAPlus.Typ/ComputablePlusCal.Expression for this pass's actual use (ComputableGuardedPlusCal below), the same way Core/ComputablePlusCal/Syntax.lean pins the shared ElaboratedPlusCal layer rather than forking a monomorphic copy.

structure GuardedPlusCal.Block (α : Bool → Type) (b : Bool) : Type

A (possibly empty) sequence of non-terminal α false objects followed by a potentially terminal α b. Generic over the index family α itself, not Typ/Expr — see the module doc above.

• begin : List (α false)
• last : α b

@[implicit_reducible]

instance GuardedPlusCal.instReprBlock {α : Bool → Type} [(b : Bool) → Repr (α b)] {b : Bool} : Repr (Block α b)

deriving Repr can't discharge this — α's Repr instance is only known per-index (∀ b, Repr (α b)), not as one instance for the whole family.

Equations

• GuardedPlusCal.instReprBlock = { reprPrec := fun (B : GuardedPlusCal.Block α b) (n : ℕ) => reprPrec (B.begin, B.last) n }

def GuardedPlusCal.Block.map {α β : Bool → Type} (f : ⦃b : Bool⦄ → α b → β b) {b : Bool} (B : Block α b) : Block β b

Equations

• GuardedPlusCal.Block.map f B = { begin := f <$> B.begin, last := f B.last }

def GuardedPlusCal.Block.traverse {α β : Bool → Type} {m : Type → Type} [Applicative m] (f : ⦃b : Bool⦄ → α b → m (β b)) {b : Bool} (B : Block α b) : m (Block β b)

Equations

• GuardedPlusCal.Block.traverse f B = GuardedPlusCal.Block.mk <$> List.traverse f B.begin <*> f B.last

Block's list-like interface. end/cons are the constructors the semantics recurses on; toList/ofList are the two halves of the isomorphism with non-empty lists; concat/prepend extend a block on the right and on the left. All abbrevs or @[reducible] so that rw sees through them in Semantics/Lemmas.lean.

@[reducible, inline]

abbrev GuardedPlusCal.Block.end {α : Bool → Type} {b : Bool} (S : α b) : Block α b

The one-statement block: nothing before the (possibly terminal) S.

Equations

• GuardedPlusCal.Block.end S = { begin := [], last := S }

@[reducible, inline]

abbrev GuardedPlusCal.Block.cons {α : Bool → Type} {b : Bool} (S : α false) (B : Block α b) : Block α b

S prefixed onto B. S is necessarily non-terminal.

Equations

• GuardedPlusCal.Block.cons S B = { begin := S :: B.begin, last := B.last }

@[reducible, inline]

abbrev GuardedPlusCal.Block.toList {α : Bool → Type} (B : Block α false) : List (α false)

Every statement of a non-terminal block, in program order.

Equations

• B.toList = B.begin.concat B.last

def GuardedPlusCal.Block.ofList {α : Bool → Type} (xs : List (α false)) (xs_nonempty : xs ≠ []) : Block α false

Inverse of Block.toList: a non-empty list read as a block.

Equations

• GuardedPlusCal.Block.ofList xs xs_nonempty = { begin := xs.dropLast, last := xs.getLast xs_nonempty }

@[reducible]

def GuardedPlusCal.Block.concat {α : Bool → Type} {b : Bool} (B : Block α false) (S : α b) : Block α b

B extended on the right by a (possibly terminal) S, which becomes the new last.

Equations

• B.concat S = { begin := B.toList, last := S }

def GuardedPlusCal.Block.prepend {α : Bool → Type} {b : Bool} (xs : List (α false)) (B : Block α b) : Block α b

B extended on the left by xs.

Equations

• GuardedPlusCal.Block.prepend xs B = { begin := xs ++ B.begin, last := B.last }

@[reducible, inline]

abbrev GuardedPlusCal.Ref (Typ Expr : Type) : Type

Equations

• GuardedPlusCal.Ref Typ Expr = ElaboratedPlusCal.Ref Typ Expr

@[reducible, inline]

abbrev GuardedPlusCal.Multicast (Typ Expr : Type) : Type

Equations

• GuardedPlusCal.Multicast Typ Expr = CorePlusCal.Multicast Typ Expr

def GuardedPlusCal.Ref.bimap {Typ Typ' Expr Expr' : Type} (f : Typ → Typ') (g : Expr → Expr') (r : Ref Typ Expr) : Ref Typ' Expr'

ElaboratedPlusCal.Ref carries no Bifunctor/Bitraversable instance (it has an extra baseType : τ field, same reason Typed2Computable/PlusCal.lean's Ref.toComputable is hand-written rather than a generic bitraverse call) — small local helpers instead, used only by Statement's instances below, not registered as global instances.

Equations

• GuardedPlusCal.Ref.bimap f g r = { name := r.name, args := Sum.map id g <$> r.args, baseType := f r.baseType }

def GuardedPlusCal.Ref.bitraverse {Typ Typ' Expr Expr' : Type} {m : Type → Type} [Applicative m] (f : Typ → m Typ') (g : Expr → m Expr') (r : Ref Typ Expr) : m (Ref Typ' Expr')

Equations

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

inductive GuardedPlusCal.Statement (Typ Expr : Type) : Bool → Bool → Type

A statement in the Guarded PlusCal language. The first Bool (guardClass) is true for a statement allowed in a branch's precondition (with/await/receive); the second (terminal) is true only for goto, which always ends a branch's action block.

• with {Typ Expr : Type} (name : String) (ann : Typ) (bound : Bool) (e : Expr) : Statement Typ Expr true false

  Body-less: a with's nested body is un-nested into flat sequencing by 𝒞_flat/𝒞_reord before reaching this type (bound is true for =, false for ∈). ann carries name's type through unchanged from ComputablePlusCal.Statement.with — every earlier pass keeps a fresh binder's type available this way, so this stage shouldn't be the one that drops it.

• await {Typ Expr : Type} (e : Expr) : Statement Typ Expr true false
• receive {Typ Expr : Type} (c r : Ref Typ Expr) (coe : TypedTLAPlus.Coercion) : Statement Typ Expr true false
• skip {Typ Expr : Type} : Statement Typ Expr false false
• print {Typ Expr : Type} (e : Expr) : Statement Typ Expr false false
• assert {Typ Expr : Type} (e : Expr) : Statement Typ Expr false false
• send {Typ Expr : Type} (c : Ref Typ Expr) (e : Expr) : Statement Typ Expr false false
• multicast {Typ Expr : Type} (c : String) (filter : Multicast Typ Expr) : Statement Typ Expr false false
• assign {Typ Expr : Type} (r : Ref Typ Expr) (e : Expr) : Statement Typ Expr false false

  Single target — parallel assignment is eliminated by 𝒞_par before reaching this type.

• goto {Typ Expr : Type} (label : String) : Statement Typ Expr false true

def GuardedPlusCal.instReprStatement.repr {Typ✝ Expr✝ : Type} {a✝ a✝¹ : Bool} [Repr Typ✝] [Repr Expr✝] : Statement Typ✝ Expr✝ a✝ a✝¹ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instReprStatement {Typ✝ Expr✝ : Type} {a✝ a✝¹ : Bool} [Repr Typ✝] [Repr Expr✝] : Repr (Statement Typ✝ Expr✝ a✝ a✝¹)

Equations

• GuardedPlusCal.instReprStatement = { reprPrec := GuardedPlusCal.instReprStatement.repr }

def GuardedPlusCal.Statement.boundName? {Typ Expr : Type} {b b' : Bool} : Statement Typ Expr b b' → Option String

The one name a statement binds, if any — with's binder, and nothing else. Lives here rather than beside either of its users because both WellFormedness.WellScoped.GuardedPlusCal (where a binder must be fresh against the enclosing scope) and Guarded2Network's Fresh (where a binder must not shadow the pass's generated inbox) need exactly this, and stating it twice is how the two drift. Stated for every guard class, since only Guarded2Network needs the action one and the answer there is always none.

Equations

• (GuardedPlusCal.Statement.with name ann bound e).boundName? = some name
• x✝.boundName? = none

@[implicit_reducible]

instance GuardedPlusCal.instInhabitedStatementFalseTrue {Typ Expr : Type} : Inhabited (Statement Typ Expr false true)

Equations

• GuardedPlusCal.instInhabitedStatementFalseTrue = { default := GuardedPlusCal.Statement.goto Inhabited.default }

@[implicit_reducible]

instance GuardedPlusCal.instInhabitedStatementTrueFalse {Typ Expr : Type} [Inhabited Expr] : Inhabited (Statement Typ Expr true false)

Equations

• GuardedPlusCal.instInhabitedStatementTrueFalse = { default := GuardedPlusCal.Statement.await Inhabited.default }

@[implicit_reducible]

instance GuardedPlusCal.instInhabitedStatementFalse {Typ Expr : Type} : Inhabited (Statement Typ Expr false false)

Equations

• GuardedPlusCal.instInhabitedStatementFalse = { default := GuardedPlusCal.Statement.skip }

@[implicit_reducible]

instance GuardedPlusCal.instBifunctorStatement {b b' : Bool} : Bifunctor fun (x1 x2 : Type) => Statement x1 x2 b b'

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instBitraversableStatement {b b' : Bool} : Bitraversable fun (x1 x2 : Type) => Statement x1 x2 b b'

Equations

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

structure GuardedPlusCal.AtomicBranch (Typ Expr : Type) : Type

• precondition : Option (Block (Statement Typ Expr true) false)
• action : Block (Statement Typ Expr false) true

@[implicit_reducible]

instance GuardedPlusCal.instReprAtomicBranch {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Repr (AtomicBranch Typ✝ Expr✝)

Equations

• GuardedPlusCal.instReprAtomicBranch = { reprPrec := GuardedPlusCal.instReprAtomicBranch.repr }

def GuardedPlusCal.instReprAtomicBranch.repr {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : AtomicBranch Typ✝ Expr✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instBifunctorAtomicBranch : Bifunctor AtomicBranch

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instBitraversableAtomicBranch : Bitraversable AtomicBranch

Equations

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

structure GuardedPlusCal.AtomicBlock (Typ Expr : Type) : Type

• label : String
• branches : List (AtomicBranch Typ Expr)

def GuardedPlusCal.instReprAtomicBlock.repr {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : AtomicBlock Typ✝ Expr✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instReprAtomicBlock {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Repr (AtomicBlock Typ✝ Expr✝)

Equations

• GuardedPlusCal.instReprAtomicBlock = { reprPrec := GuardedPlusCal.instReprAtomicBlock.repr }

@[implicit_reducible]

instance GuardedPlusCal.instBifunctorAtomicBlock : Bifunctor AtomicBlock

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instBitraversableAtomicBlock : Bitraversable AtomicBlock

Equations

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

@[reducible, inline]

abbrev GuardedPlusCal.Thread (Typ Expr : Type) : Type

One parallel {...} thread — a sequence of labelled atomic blocks, in program order. AtomicBlock already carries a label, unlike ElaboratedPlusCal.Process.threads's List (String × Block τ ε true) pairing, so no separate label pairing is needed here.

Equations

• GuardedPlusCal.Thread Typ Expr = List (GuardedPlusCal.AtomicBlock Typ Expr)

structure GuardedPlusCal.Declarations (Typ Expr : Type) : Type

What a scope declares: its variables with their initializers, its channels, and its FIFOs.

• variables : List (String × Typ × Bool × Option (Bool × Expr))
• channels : List (String × Typ × List Expr)
• fifos : List (String × Typ × List Expr)

def GuardedPlusCal.instReprDeclarations.repr {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Declarations Typ✝ Expr✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instReprDeclarations {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Repr (Declarations Typ✝ Expr✝)

Equations

• GuardedPlusCal.instReprDeclarations = { reprPrec := GuardedPlusCal.instReprDeclarations.repr }

@[implicit_reducible]

instance GuardedPlusCal.instBifunctorDeclarations : Bifunctor Declarations

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instBitraversableDeclarations : Bitraversable Declarations

Equations

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

structure GuardedPlusCal.Process (Typ Expr : Type) : Type

A declared process: its optional mailbox, its fairness, its identity, its own declarations, and its parallel threads, each a Thread Typ Expr of self-labelled atomic blocks.

• mailbox : Option (String × List Expr)
• isFair : Bool
• name : String
• =|∈ : Bool
• id : Expr
• localState : Declarations Typ Expr
• threads : List (Thread Typ Expr)

def GuardedPlusCal.instReprProcess.repr {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Process Typ✝ Expr✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instReprProcess {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Repr (Process Typ✝ Expr✝)

Equations

• GuardedPlusCal.instReprProcess = { reprPrec := GuardedPlusCal.instReprProcess.repr }

@[implicit_reducible]

instance GuardedPlusCal.instBifunctorProcess : Bifunctor Process

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instBitraversableProcess : Bitraversable Process

Equations

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

structure GuardedPlusCal.Algorithm (Typ Expr : Type) : Type

• isFair : Bool
• name : String
• globalState : Declarations Typ Expr
• processes : List (Process Typ Expr)

def GuardedPlusCal.instReprAlgorithm.repr {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Algorithm Typ✝ Expr✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instReprAlgorithm {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Repr (Algorithm Typ✝ Expr✝)

Equations

• GuardedPlusCal.instReprAlgorithm = { reprPrec := GuardedPlusCal.instReprAlgorithm.repr }

@[implicit_reducible]

instance GuardedPlusCal.instBifunctorAlgorithm : Bifunctor Algorithm

Equations

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

@[implicit_reducible]

instance GuardedPlusCal.instBitraversableAlgorithm : Bitraversable Algorithm

Equations

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

@[reducible, inline]

abbrev ComputableGuardedPlusCal.Ref : Type

Equations

• ComputableGuardedPlusCal.Ref = GuardedPlusCal.Ref ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableGuardedPlusCal.Multicast : Type

Equations

• ComputableGuardedPlusCal.Multicast = GuardedPlusCal.Multicast ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableGuardedPlusCal.Statement : Bool → Bool → Type

Equations

• ComputableGuardedPlusCal.Statement = GuardedPlusCal.Statement ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableGuardedPlusCal.AtomicBranch : Type

Equations

• ComputableGuardedPlusCal.AtomicBranch = GuardedPlusCal.AtomicBranch ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableGuardedPlusCal.AtomicBlock : Type

Equations

• ComputableGuardedPlusCal.AtomicBlock = GuardedPlusCal.AtomicBlock ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableGuardedPlusCal.Thread : Type

Equations

• ComputableGuardedPlusCal.Thread = GuardedPlusCal.Thread ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableGuardedPlusCal.Declarations : Type

Equations

• ComputableGuardedPlusCal.Declarations = GuardedPlusCal.Declarations ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableGuardedPlusCal.Process : Type

Equations

• ComputableGuardedPlusCal.Process = GuardedPlusCal.Process ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableGuardedPlusCal.Algorithm : Type

Equations

• ComputableGuardedPlusCal.Algorithm = GuardedPlusCal.Algorithm ComputableTLAPlus.Typ ComputablePlusCal.Expression