Guarded2Network compiles a receive away entirely, replacing it with a real second kind of thread (NetworkPlusCal.Thread.rx) that loops draining a fresh process-local inbox sequence variable, and rewrites every later await/with guard that referenced the received value to read inbox instead — the guard's truth no longer depends on an abstract "did a message arrive" primitive, only on ordinary sequence operations (Head/Tail/Len) over inbox.

• Monad-polymorphic: {m} [Monad m] [MonadFresh m] [MonadDiagnostic Empty G2NError m], the same DiagT-based calling convention every other diagnostics-producing pass uses. Empty for the warning channel: this pass reports no warnings.
• Every fresh name — the process-local inbox variable and each .rx thread's own block label — comes from freshName (Common/Fresh.lean), giving the same $-based hygiene as every other pass's fresh binder: a name a real user could have written can never collide with one of these. inbox is fresh once per process, shared by every thread of that process; each new .rx thread gets its own fresh label. That label is what the semantics schedules the receiving loop by, and what its own terminal goto targets; it must therefore stay distinct from every AtomicBlock.label in the process, which freshName guarantees.
• A receive's stored Coercion (Core/TypedTLAPlus/Coercion.lean) is discharged via Coercion.applyComputable directly against the built Head(inbox) expression, not left unapplied.
• Only G2NError.internalInvariantViolated guards a receive's channel resolution — and only "channel not found" is actually reachable: GuardedPlusCal.Declarations.channels/ .fifos already store a channel's checked element type directly (Elaborator/ PlusCal.lean's checkChannelDecl unwraps Channel(τ)/dom → Channel(τ) down to τ before it reaches Declarations), so there's no wrapped Typ left to mismatch on by the time this pass runs.
• Guard-expression substitution reuses ComputableTLAPlus.Expression.substRef (Core/ComputableTLAPlus/Subst.lean, already written for Computable2Guarded/FlatReord.lean's own 𝒞_reord case): bare r substitutes the name directly; a compound r substitutes the whole base variable with a one-entry EXCEPT. Fold direction matters: each new (Ref, Expr) pair is appended to the end of newInstrs as its receive is processed, and a later guard's substitution is a foldr over that list — a later-appended "advance inbox past what this receive consumed" pair applies before an earlier-appended one (since foldr processes right-to-left), which is what makes a second receive's freshly-substituted Head(inbox) get caught and advanced to Head(Tail(inbox)) by the first receive's still-pending advance. Switching to foldl silently breaks this.
• Positions are carried across, not dropped: every NetworkPlusCal.Statement this pass builds is registered (@@) at the GuardedPlusCal.Statement it replaces, and the consumption assignments a receive compiles into take that receive's own span. An unregistered node is one posOf answers for with an unrelated node's span.

receive(c, x[0]);
await x[0] + y = 0;
receive(c, y);
await x[0] + y = 0;

compiles to (guards, symbolically, before any assignment runs):

await Len(inbox) > 0;
await [x EXCEPT ![0] = Head(inbox)][0] + y = 0;
await Len(inbox) > 1;
await [x EXCEPT ![0] = Head(inbox)][0] + Head(Tail(inbox)) = 0;

and the branch's action block gains, as its own new prefix (ordinary sequential assignments — no substitution needed here, since each one's Head(inbox) is read after the previous one's own inbox := Tail(inbox) has already run):

x[0] := Head(inbox); inbox := Tail(inbox); y := Head(inbox); inbox := Tail(inbox);

@[reducible, inline]

abbrev Guarded2NetworkChans : Type

One process's channel/fifo element-type table — a channel name resolves to its already-checked element type directly (see the module doc above for why no wrapped Channel(_)/dom → Channel(_) shape ever needs matching here), built by merging global and process-local channels/fifos declarations. Looked up by a receive's channel Ref's base name, ignoring any index arguments — a channel's element type doesn't depend on which array slot is referenced.

Equations

• Guarded2NetworkChans = List (String × ComputableTLAPlus.Typ)

The three sequence expressions this pass builds over inbox. Public, and namespaced rather than file-private, because the refinement proof has to state what they mean — Guarded2Network/ Lemmas/Seq.lean's SeqBuiltins gives each one its evaluation law, and a law about a private definition cannot be written at all.

def Guarded2Network.head (τ : ComputableTLAPlus.Typ) (e : ComputablePlusCal.Expression) : ComputablePlusCal.Expression

Head(e).

Equations

• Guarded2Network.head τ e = (ComputableTLAPlus.Expression.var (SurfaceTLAPlus.Typ.operator [SurfaceTLAPlus.Typ.seq τ] τ) (TypedTLAPlus.Origin.module "Sequences" "Head")).opCall [e]

def Guarded2Network.tail (τ : ComputableTLAPlus.Typ) (e : ComputablePlusCal.Expression) : ComputablePlusCal.Expression

Tail(e).

Equations

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

def Guarded2Network.lenGt (τ : ComputableTLAPlus.Typ) (e : ComputablePlusCal.Expression) (n : ℕ) : ComputablePlusCal.Expression

Len(e) > n, n a literal Nat.

Equations

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

def Guarded2Network.substGuardStmt (r : ComputableGuardedPlusCal.Ref) (rhs : ComputablePlusCal.Expression) (s : ComputableNetworkPlusCal.Statement true false) : ComputableNetworkPlusCal.Statement true false

One assignment's effect substituted into a guard-class statement — .with's bound expression or .await's condition, the only expression field either constructor carries. Delegates to ComputableTLAPlus.Expression.substRef, so a bare and a compound Ref behave here exactly as they do everywhere else substitution is applied.

Public, namespaced and @[expose] for the same reasons convertActionStmt below is: the refinement proof's reorder lemmas (Guarded2Network/Lemmas/Reorder.lean) are stated against the pass's own substitution rather than against a re-derivation of it, and their proofs reduce through this body.

Equations

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

def Guarded2Network.substGuards (newInstrs : List (ComputableGuardedPlusCal.Ref × ComputablePlusCal.Expression × SourceSpan)) (s : ComputableNetworkPlusCal.Statement true false) : ComputableNetworkPlusCal.Statement true false

Every receive processed so far (processPrecondition's newInstrs) substituted into a later guard — see the module doc's foldr/fold-direction explanation. The per-entry span plays no part in substitution and is dropped here.

Equations

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

def Guarded2Network.convertActionStmt {b : Bool} (s : ComputableGuardedPlusCal.Statement false b) : ComputableNetworkPlusCal.Statement false b

Every action-class constructor GuardedPlusCal.Statement/NetworkPlusCal.Statement share verbatim (all but receive, already compiled away above, and with, guard-class only) — Ref/ Multicast are the same types under both pinnings (Core/NetworkPlusCal/Syntax.lean reuses GuardedPlusCal.Ref/.Multicast directly), so this is a plain re-tagging, not a translation. Public and namespaced, not file-private: the refinement proof states its semantic equations (Guarded2Network/Lemmas/Statement.lean), and a lemma about a private definition cannot be written — and @[expose], so that the equations it satisfies are provable by rfl in another module rather than only inside this one.

Equations

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

def ComputableGuardedPlusCal.Thread.toNetwork {m : Type → Type} [Monad m] [MonadDiagnostic Empty G2NError m] [MonadFresh m] (chans : Guarded2NetworkChans) (inboxName : String) (T : Thread) : m (List (String × ComputableTLAPlus.Typ × Bool × Option (Bool × ComputablePlusCal.Expression)) × List ComputableNetworkPlusCal.Thread × ComputableNetworkPlusCal.Thread)

One process's channel table (already merged with that process's own local channels/fifos by Process.toNetwork) and its single shared inbox name (fresh once per process, shared by every thread of the process) drive the whole compilation: every AtomicBranch's precondition is walked (processPrecondition), its action block gets the resulting consumption assignments prepended, and a new .rx thread is added the first time this call encounters a not-yet-seen channel.

Equations

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

def ComputableGuardedPlusCal.Process.toNetwork {m : Type → Type} [Monad m] [MonadDiagnostic Empty G2NError m] [MonadFresh m] (globalChans : Guarded2NetworkChans) (p : Process) : m ComputableNetworkPlusCal.Process

Equations

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

def ComputableGuardedPlusCal.Algorithm.toNetwork {m : Type → Type} [Monad m] [MonadDiagnostic Empty G2NError m] [MonadFresh m] (algo : Algorithm) : m ComputableNetworkPlusCal.Algorithm

Equations

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