The output of Guarded2Network: a receive is no longer an abstract guard statement — it's compiled into a genuine second kind of thread, Thread.rx, that loops reading a process-local inbox sequence variable, and every later await/with guard that referenced the received value now reads that inbox instead. Reuses GuardedPlusCal.Block/Ref/Multicast/ Declarations unchanged — none of those shapes are affected by this pass, only Statement (drops receive) and Thread (gains a second, non-code constructor) are.

• No separate ChanRef type: GuardedPlusCal.Statement already reuses one uniform Ref for both a channel argument and an ordinary reference (Core/GuardedPlusCal/Syntax.lean's send/assign), so NetworkPlusCal.Statement carries that same uniformity forward.
• Real Bifunctor/Bitraversable instances throughout, matching Core/GuardedPlusCal/Syntax.lean's instances (Ref.bimap/Ref.bitraverse reused directly, since Ref itself has no generic instance).
• Thread is a genuine sum (.code (blocks : List AtomicBlock) | .rx (chan : Ref Typ Expr) (label : String) (τ : Typ) (inbox : String)) — a receiving thread is a real second kind of thread, not folded into .code.
• deriving Repr throughout — no Pretty.lean needed yet: -d dump-network renders via reprStr, the same way -d dump-guarded does today (Fugue.lean's existing debug-dump wiring). A real pretty-printer is only worth adding once a backend needs one.
• Lives under the existing Fugue.Core lean_lib target (its roots := #[Core] glob picks this file up automatically) — no new lakefile.lean target needed, unlike Fugue.G2N, already declared for the pass itself.

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

A statement in the Network PlusCal language — identical to GuardedPlusCal.Statement minus receive (compiled away into Thread.rx by this pass), including with's ann : Typ field (GuardedPlusCal.Statement.with's doc comment explains why it's kept). The first Bool (guardClass) is true for a statement allowed in a branch's precondition (with/await); the second (terminal) is true only for goto.

• with {Typ Expr : Type} (name : String) (ann : Typ) (bound : Bool) (e : Expr) : Statement Typ Expr true false
• await {Typ Expr : Type} (e : Expr) : 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 : GuardedPlusCal.Ref Typ Expr) (e : Expr) : Statement Typ Expr false false
• multicast {Typ Expr : Type} (c : String) (filter : GuardedPlusCal.Multicast Typ Expr) : Statement Typ Expr false false
• assign {Typ Expr : Type} (r : GuardedPlusCal.Ref Typ Expr) (e : Expr) : Statement Typ Expr false false
• goto {Typ Expr : Type} (label : String) : Statement Typ Expr false true

@[implicit_reducible]

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

Equations

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

def NetworkPlusCal.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 NetworkPlusCal.instInhabitedStatementFalseTrue {Typ Expr : Type} : Inhabited (Statement Typ Expr false true)

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance NetworkPlusCal.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 NetworkPlusCal.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 NetworkPlusCal.AtomicBranch (Typ Expr : Type) : Type

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

@[implicit_reducible]

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

Equations

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

def NetworkPlusCal.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 NetworkPlusCal.instBifunctorAtomicBranch : Bifunctor AtomicBranch

Equations

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

@[implicit_reducible]

instance NetworkPlusCal.instBitraversableAtomicBranch : Bitraversable AtomicBranch

Equations

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

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

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

def NetworkPlusCal.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 NetworkPlusCal.instReprAtomicBlock {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Repr (AtomicBlock Typ✝ Expr✝)

Equations

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

@[implicit_reducible]

instance NetworkPlusCal.instBifunctorAtomicBlock : Bifunctor AtomicBlock

Equations

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

@[implicit_reducible]

instance NetworkPlusCal.instBitraversableAtomicBlock : Bitraversable AtomicBlock

Equations

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

inductive NetworkPlusCal.Thread (Typ Expr : Type) : Type

One parallel {...} thread — either ordinary code (a sequence of labelled atomic blocks, in program order, same shape as GuardedPlusCal.Thread) or a dedicated receiving loop: drains chan of type τ into a process-local inbox sequence variable (fresh per process, via Guarded2Network.freshName). A real second kind of thread, not folded into .code, since its body isn't a List AtomicBlock — see the module doc.

label is the receiving loop's own block label. .rx's meaning is the single atomic block label : receive(chan, tmp) ; inbox := Append(inbox, tmp) ; goto label, without the temporary variable tmp ever being assigned to — so the loop needs a label of its own to be scheduled by, and to be the target of its own terminal goto, whereas tmp is never written and needs no name at all. Both are freshly generated, so this one field carries the one that matters.

• code {Typ Expr : Type} (blocks : List (AtomicBlock Typ Expr)) : Thread Typ Expr
• rx {Typ Expr : Type} (chan : GuardedPlusCal.Ref Typ Expr) (label : String) (τ : Typ) (inbox : String) : Thread Typ Expr

@[implicit_reducible]

instance NetworkPlusCal.instReprThread {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Repr (Thread Typ✝ Expr✝)

Equations

• NetworkPlusCal.instReprThread = { reprPrec := NetworkPlusCal.instReprThread.repr }

def NetworkPlusCal.instReprThread.repr {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Thread Typ✝ Expr✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance NetworkPlusCal.instBifunctorThread : Bifunctor Thread

Equations

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

@[implicit_reducible]

instance NetworkPlusCal.instBitraversableThread : Bitraversable Thread

Equations

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

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

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

def NetworkPlusCal.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 NetworkPlusCal.instReprProcess {Typ✝ Expr✝ : Type} [Repr Typ✝] [Repr Expr✝] : Repr (Process Typ✝ Expr✝)

Equations

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

@[implicit_reducible]

instance NetworkPlusCal.instBifunctorProcess : Bifunctor Process

Equations

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

@[implicit_reducible]

instance NetworkPlusCal.instBitraversableProcess : Bitraversable Process

Equations

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

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

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

@[implicit_reducible]

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

Equations

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

def NetworkPlusCal.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 NetworkPlusCal.instBifunctorAlgorithm : Bifunctor Algorithm

Equations

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

@[implicit_reducible]

instance NetworkPlusCal.instBitraversableAlgorithm : Bitraversable Algorithm

Equations

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

@[reducible, inline]

abbrev ComputableNetworkPlusCal.Ref : Type

Equations

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

@[reducible, inline]

abbrev ComputableNetworkPlusCal.Multicast : Type

Equations

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

@[reducible, inline]

abbrev ComputableNetworkPlusCal.Statement : Bool → Bool → Type

Equations

• ComputableNetworkPlusCal.Statement = NetworkPlusCal.Statement ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableNetworkPlusCal.AtomicBranch : Type

Equations

• ComputableNetworkPlusCal.AtomicBranch = NetworkPlusCal.AtomicBranch ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableNetworkPlusCal.AtomicBlock : Type

Equations

• ComputableNetworkPlusCal.AtomicBlock = NetworkPlusCal.AtomicBlock ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableNetworkPlusCal.Thread : Type

Equations

• ComputableNetworkPlusCal.Thread = NetworkPlusCal.Thread ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableNetworkPlusCal.Declarations : Type

Equations

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

@[reducible, inline]

abbrev ComputableNetworkPlusCal.Process : Type

Equations

• ComputableNetworkPlusCal.Process = NetworkPlusCal.Process ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputableNetworkPlusCal.Algorithm : Type

Equations

• ComputableNetworkPlusCal.Algorithm = NetworkPlusCal.Algorithm ComputableTLAPlus.Typ ComputablePlusCal.Expression