The denotational semantics of Network PlusCal. Statement here is GuardedPlusCal.Statement minus receive, so every case below is that language's case verbatim — see Core/GuardedPlusCal/Semantics/Denotational.lean's module doc for what reducing/aborting/ diverging mean and why blocking and aborting are kept distinct.

The state space is shared, not re-declared: Behavior, ChanKey, FIFOs, LocalState, EvalStep and Ref.pathAborts are taken from GuardedPlusCal unchanged. This pass does not touch memories, channels or references — it only moves a receive out of the guard position and into a Thread.rx. Sharing the state space is also what lets a refinement between the two languages be stated without first transporting across two isomorphic copies of the same types.

Reduction of statements

def NetworkPlusCal.Statement.reducing {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) {b b' : Bool} : ComputableNetworkPlusCal.Statement b b' → Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V × GuardedPlusCal.LocalState V)

Equations

• One or more equations did not get rendered due to their size.
• NetworkPlusCal.Statement.reducing Ξ Ω (NetworkPlusCal.Statement.await e) = NetworkPlusCal.Statement.reducing.test Ξ Ω e ComputableTLAPlus.ExprSemantics.tru
• NetworkPlusCal.Statement.reducing Ξ Ω NetworkPlusCal.Statement.skip = NetworkPlusCal.Statement.reducing.idle
• NetworkPlusCal.Statement.reducing Ξ Ω (NetworkPlusCal.Statement.assert e) = NetworkPlusCal.Statement.reducing.test Ξ Ω e ComputableTLAPlus.ExprSemantics.tru
• NetworkPlusCal.Statement.reducing Ξ Ω (NetworkPlusCal.Statement.multicast c filter) = ∅

def NetworkPlusCal.Statement.reducing.test {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (e : ComputablePlusCal.Expression) (v : V) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V × GuardedPlusCal.LocalState V)

test e v is the identity transition restricted to states that evaluate e to v.

Equations

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

def NetworkPlusCal.Statement.reducing.idle {V : Type u} : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V × GuardedPlusCal.LocalState V)

The identity transition, i.e. nothing is performed.

Equations

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

def NetworkPlusCal.Statement.aborting {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) {b b' : Bool} : ComputableNetworkPlusCal.Statement b b' → Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

Equations

• One or more equations did not get rendered due to their size.
• NetworkPlusCal.Statement.aborting Ξ Ω NetworkPlusCal.Statement.skip = ∅
• NetworkPlusCal.Statement.aborting Ξ Ω (NetworkPlusCal.Statement.goto label) = ∅
• NetworkPlusCal.Statement.aborting Ξ Ω (NetworkPlusCal.Statement.multicast c filter) = ∅

def NetworkPlusCal.Statement.diverging {V : Type u} {b b' : Bool} : ComputableNetworkPlusCal.Statement b b' → Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

No statement can diverge — same as on the Guarded side.

Equations

• NetworkPlusCal.Statement.diverging x✝ = ∅

def NetworkPlusCal.Statement.blocking {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) {b b' : Bool} : ComputableNetworkPlusCal.Statement b b' → Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

The states from which a guard-class statement is blocked — same as on the Guarded side, minus receive (this language has none): await on a boolean that is not TRUE, or with x ∈ e on a (present but) empty set. The trace is 1.

Equations

• One or more equations did not get rendered due to their size.
• NetworkPlusCal.Statement.blocking Ξ Ω x✝ = ∅

Reduction of blocks and atomic branches

GuardedPlusCal.Block.reducing/.aborting/.diverging are generic in the statement family, so they are applied here directly rather than restated.

def NetworkPlusCal.Statement.blockReducing {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) {g b : Bool} (B : GuardedPlusCal.Block (ComputableNetworkPlusCal.Statement g) b) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V × GuardedPlusCal.LocalState V)

A block of Network PlusCal statements, all of guard class g.

Equations

• NetworkPlusCal.Statement.blockReducing Ξ Ω B = GuardedPlusCal.Block.reducing (fun ⦃x : Bool⦄ => NetworkPlusCal.Statement.reducing Ξ Ω) B

def NetworkPlusCal.Statement.blockAborting {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) {g b : Bool} (B : GuardedPlusCal.Block (ComputableNetworkPlusCal.Statement g) b) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

A block of Network PlusCal statements, all of guard class g.

Equations

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

def NetworkPlusCal.Statement.blockDiverging {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) {g b : Bool} (B : GuardedPlusCal.Block (ComputableNetworkPlusCal.Statement g) b) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

A block of Network PlusCal statements, all of guard class g.

Equations

• NetworkPlusCal.Statement.blockDiverging Ξ Ω B = GuardedPlusCal.Block.diverging (fun ⦃x : Bool⦄ => NetworkPlusCal.Statement.diverging) (fun ⦃x : Bool⦄ => NetworkPlusCal.Statement.reducing Ξ Ω) B

def NetworkPlusCal.Statement.blockBlocking {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) {g b : Bool} (B : GuardedPlusCal.Block (ComputableNetworkPlusCal.Statement g) b) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

A block of Network PlusCal statements, all of guard class g.

Equations

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

def NetworkPlusCal.Statement.listReducing {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) {g : Bool} (A : List (ComputableNetworkPlusCal.Statement g false)) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V × GuardedPlusCal.LocalState V)

A possibly-empty list of Network PlusCal statements — see GuardedPlusCal.Block.listReducing for why the shape exists alongside Block. Guarded2Network prepends one of these (a branch's consumption assignments) to an action block, and its refinement proof states the two factors separately.

Equations

• NetworkPlusCal.Statement.listReducing Ξ Ω A = GuardedPlusCal.Block.listReducing (fun ⦃x : Bool⦄ => NetworkPlusCal.Statement.reducing Ξ Ω) A

def NetworkPlusCal.Statement.listAborting {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) {g : Bool} (A : List (ComputableNetworkPlusCal.Statement g false)) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

A possibly-empty list of Network PlusCal statements — see GuardedPlusCal.Block.listReducing for why the shape exists alongside Block. Guarded2Network prepends one of these (a branch's consumption assignments) to an action block, and its refinement proof states the two factors separately.

Equations

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

def NetworkPlusCal.Statement.listDiverging {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) {g : Bool} (A : List (ComputableNetworkPlusCal.Statement g false)) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

A possibly-empty list of Network PlusCal statements — see GuardedPlusCal.Block.listReducing for why the shape exists alongside Block. Guarded2Network prepends one of these (a branch's consumption assignments) to an action block, and its refinement proof states the two factors separately.

Equations

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

def NetworkPlusCal.Statement.listBlocking {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) {g : Bool} (A : List (ComputableNetworkPlusCal.Statement g false)) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

A possibly-empty list of Network guards, blocked: some prefix reduces to a state at which the next guard blocks — the list counterpart of Statement.blockBlocking, mirroring Statement.listAborting.

Equations

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

def NetworkPlusCal.AtomicBranch.reducing {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (B : ComputableNetworkPlusCal.AtomicBranch) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V × GuardedPlusCal.LocalState V)

Equations

• NetworkPlusCal.AtomicBranch.reducing Ξ Ω B = B.precondition.elim Relation.Idle (NetworkPlusCal.Statement.blockReducing Ξ Ω) ∘ᵣ₂ NetworkPlusCal.Statement.blockReducing Ξ Ω B.action

def NetworkPlusCal.AtomicBranch.aborting {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (B : ComputableNetworkPlusCal.AtomicBranch) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

Equations

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

def NetworkPlusCal.AtomicBranch.diverging {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (B : ComputableNetworkPlusCal.AtomicBranch) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

Equations

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

def NetworkPlusCal.AtomicBranch.blocking {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (B : ComputableNetworkPlusCal.AtomicBranch) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

The states from which an atomic branch is blocked: its precondition reduces to a state at which some later guard blocks. A bare action blocks nowhere.

Equations

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

Reduction of atomic blocks

A block picks one of its branches nondeterministically — reducing/aborting/diverging as some branch, chosen from B.branches. Only needed on the NetworkPlusCal side: the refinement relation's target type is what needs the flat state encoding uniformly, the source stays quantified throughout since it is only ever existentially bound, never required to match the target's type. GuardedPlusCal therefore has no AtomicBlock semantics at all.

def NetworkPlusCal.AtomicBlock.reducing {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (B : ComputableNetworkPlusCal.AtomicBlock) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V × GuardedPlusCal.LocalState V)

Equations

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

def NetworkPlusCal.AtomicBlock.aborting {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (B : ComputableNetworkPlusCal.AtomicBlock) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

Equations

• NetworkPlusCal.AtomicBlock.aborting Ξ Ω B = {(σ, ε) : GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V | ∃ Br ∈ B.branches, (σ, ε) ∈ NetworkPlusCal.AtomicBranch.aborting Ξ Ω Br}

def NetworkPlusCal.AtomicBlock.diverging {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (B : ComputableNetworkPlusCal.AtomicBlock) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

Equations

• NetworkPlusCal.AtomicBlock.diverging Ξ Ω B = {(σ, ε) : GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V | ∃ Br ∈ B.branches, (σ, ε) ∈ NetworkPlusCal.AtomicBranch.diverging Ξ Ω Br}

def NetworkPlusCal.AtomicBlock.blocking {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (B : ComputableNetworkPlusCal.AtomicBlock) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V)

A block is blocked iff every one of its branches is: either is angelic, so it proceeds on any branch that can and blocks only when none can — the intersection over B.branches, where reducing/aborting/diverging take the union.

Equations

• NetworkPlusCal.AtomicBlock.blocking Ξ Ω B = {x : GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V | ∀ Br ∈ B.branches, x ∈ NetworkPlusCal.AtomicBranch.blocking Ξ Ω Br}

Threads

A .code thread has no denotation of its own. A process state is a memory together with a set of labels — at most one per thread — and one process step picks an enabled label l from that set, runs the atomic block the label names, and replaces l by the label the block's terminal goto jumped to. So a .code thread contributes exactly two things: the labels it owns, and the block each of those labels names. Everything else is the process- and algorithm-level fixed points.

Thread.rx is different. It owns no label, and its step consumes and produces none: it is a virtual thread whose meaning is the single step "read the head message off mailboxₚ and append it to inboxₚ", taken whenever mailboxₚ is non-empty and with no tmpₚ variable — the value goes straight from the channel into inboxₚ. It contributes one thing: Thread.rxStep, a label-free reducing step handed to the process layer through CodeTable.relay. Thread.rx's label field names the Go loop the thread compiles to and has no part in this semantics.

def NetworkPlusCal.Thread.labels : ComputableNetworkPlusCal.Thread → List String

The labels a thread owns. A .code thread owns its blocks' labels; a .rx thread owns none — its step is label-free.

Equations

• (NetworkPlusCal.Thread.code blocks).labels = List.map (fun (x : NetworkPlusCal.AtomicBlock ComputableTLAPlus.Typ ComputablePlusCal.Expression) => x.label) blocks
• (NetworkPlusCal.Thread.rx chan label τ inbox).labels = []

def NetworkPlusCal.Thread.rxStep {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (chan : ComputableNetworkPlusCal.Ref) (inbox : String) : Set (GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V × GuardedPlusCal.LocalState V)

The one reducing step a receiving thread contributes: read the head message off chan and append it to the inbox sequence, leaving every scheduled label untouched. Written directly rather than built from Statements, because NetworkPlusCal.Statement has no receive and the paper's tmpₚ is never assigned.

The step is silent: reception is not in Behavior's alphabet (GuardedPlusCal's Semantics/Denotational.lean). Moving a message from chan into inbox changes no observable; that the two together hold what the source's channel holds is the refinement invariant's job. An empty channel yields no step — a receiving thread then waits, which the blocking semantics records.

Equations

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