The denotational semantics of Guarded PlusCal, as three relations per syntactic form: reducing (a step to a successor state, emitting a list of observable behaviors), aborting (a state from which the form goes wrong), and diverging (a state from which it runs forever).

They are plain definitions rather than Reduce/Abort/Diverge instances, so the ⟦·⟧*/⟦·⟧⊥/⟦·⟧∞ notations do not apply here. Those classes take their second argument as an outParam, and with the value type abstract it occurs only there — nothing in a Statement or an AtomicBranch mentions it — so Lean cannot order the synthesis of the ExprSemantics argument. Nothing needs the classes: StrongRefinement takes the relations as plain Sets. The instances can be registered later, against the concrete TLA⁺ value type.

Blocking and aborting are deliberately different: a statement with no reducing transition and no aborting state is a guard that is simply not enabled yet, which is what await, receive on an empty FIFO, and with x ∈ {} all are. That distinction is why ExprSemantics exposes isBool and isSet — without them a non-boolean guard would be indistinguishable from a false one.

The expression layer underneath is abstract (ComputableTLAPlus.ExprSemantics), to be refined to the real TLA⁺ semantics later; see that file's module doc.

Channels are kept out of the main memory, in a separate FIFOs map, so a local state is a variable memory beside a channel memory. An expression that reaches into a channel therefore has no meaning at all here rather than a wrong one, which is what lets the expression layer stay ignorant of channels entirely.

This file stops at AtomicBranch. Threads, processes and algorithms are above it: a thread has no denotation of its own, only the labels it owns, and the process and algorithm layers are defined by fixed points over a step relation. See Core/NetworkPlusCal/Semantics/Denotational.lean's Thread.labels.

Failure modes a well-formedness side condition could assume away are stated instead: a receive with a bad channel, an await on a non-boolean and a with x ∈ e on a non-set all abort here rather than blocking or being ruled out by assumption.

@[reducible, inline]

abbrev GuardedPlusCal.ChanKey (V : Type u) : Type u

The key identifying a single FIFO: the channel's name together with its resolved index path. Only the name and the evaluated indices are observable, and this is also the shape a Behavior.send reports.

Equations

• GuardedPlusCal.ChanKey V = (String × List (ComputableTLAPlus.PathStep V))

def GuardedPlusCal.selfName : String

The name a process instance's own identity is bound to, matching Elaborator/PlusCal.lean's extend "self" .address.

Equations

• GuardedPlusCal.selfName = "self"

inductive GuardedPlusCal.Behavior (V : Type u) : Type u

One of the possible observable behaviors exhibited by PlusCal statements. Every event carries the process instance that emitted it — the value bound to selfName in its memory — so that program order within one process is recoverable from a trace that interleaves several. Without it, two prints from different processes would be indistinguishable from two prints of the same process, and their relative order would stop being observable.

send additionally carries the channel it pushes onto.

Reception is not an event. The alphabet is exactly print and send, and a recv event would be unsound as an observation of the source program: Guarded2Network defers consumption to a .rx thread that pops the channel ahead of the block that uses the value, so a block whose guard never holds — l: receive(ch, x) ; await FALSE ; goto l' — pops a message in the target while the source block never reduces at all and so never emits anything. No relation up to reordering repairs that: the target event has no source counterpart to be reordered against. What ties the channel's contents to the target's inbox is the refinement invariant relatesTo, per channel.

• print {V : Type u} (p v : V) : Behavior V
• send {V : Type u} (p : V) (c : ChanKey V) (v : V) : Behavior V

@[reducible, inline]

abbrev GuardedPlusCal.Trace (V : Type u) : Type u

The trace alphabet: a possibly-infinite sequence of observable events. Monoid (Seq α) makes it the ordered monoid traces are composed in.

Possibly-infinite and not List, even though no statement or block can emit an infinite trace — Statement.diverging is ∅ and a block is finite, so divergence enters only at Algebra (Semantics/Process.lean). A diverging algorithm that keeps sending emits forever, and a List cannot hold what it emits: with a finite trace type Algebra.diverging could only contain executions that fall silent after finitely many events, so every productive divergence would be absent from the denotation outright.

The type is uniform across the statement, block and algorithm layers rather than finite below and infinite above, so no layer boundary carries a Seq.ofList coercion. Finiteness of the reducing and aborting traces is a derived property rather than a typing constraint: nothing downstream needs it, and no proof relies on cancellativity (Seq has none — an infinite left factor absorbs its right factor, mul_eq_left_of_not_terminates).

Equations

• GuardedPlusCal.Trace V = Stream'.Seq (GuardedPlusCal.Behavior V)

@[reducible, inline]

abbrev GuardedPlusCal.FIFOs (V : Type u) : Type u

The global map containing FIFOs. Pushes go on the right, pops come off the left.

Finmap for the reason Memory is one (Core/ComputableTLAPlus/Semantics/Interface.lean): key order is not observable, and letting it into the type turns commutation lemmas false. Updating a channel is insert rather than AList.replace — every rule below establishes F.lookup k = some _ before writing k, so the two agree wherever either is reached, and insert is the one with a usable lookup equation (= some v, not v <$ lookup k F).

Equations

• GuardedPlusCal.FIFOs V = Finmap fun (x : GuardedPlusCal.ChanKey V) => List V

@[reducible, inline]

abbrev GuardedPlusCal.LocalState (V : Type u) : Type u

The local reduction state of an atomic block: the process's own memory, the channels, and a label field that is none while running and some l once a terminal goto has jumped to l. Statement b b' already tracks terminality syntactically and the reduction relations pin the label field's value (none on every source state, some _ only on a goto's target), so nothing is gained by also carrying it at the type level — see Statement.reducing below.

There is deliberately no third component for with-bound temporaries. That an assignment does not target a block-local binder is a syntactic property, checked by WellFormedness; keeping it in the state would oblige every lemma to translate between two state shapes for no proof-side gain.

Equations

• GuardedPlusCal.LocalState V = (ComputableTLAPlus.Memory V × GuardedPlusCal.FIFOs V × Option String)

Named projections. LocalState is a nested anonymous product, so its components are otherwise reachable only as σ.1/σ.2.1/σ.2.2 or by destructuring at every binding site. Named projections let a proof intro σₜ σₜ' ε σₛ with no pattern at all and reach components by name, destructuring only where it genuinely case-splits on the label.

def GuardedPlusCal.LocalState.mem {V : Type u} (σ : LocalState V) : ComputableTLAPlus.Memory V

The memory component.

Equations

• σ.mem = σ.1

def GuardedPlusCal.LocalState.fifos {V : Type u} (σ : LocalState V) : FIFOs V

The FIFO component.

Equations

• σ.fifos = σ.2.1

def GuardedPlusCal.LocalState.label {V : Type u} (σ : LocalState V) : Option String

The label component: none while running, some l once the block has jumped to l.

Equations

• σ.label = σ.2.2

@[simp]

theorem GuardedPlusCal.LocalState.mem_mk {V : Type u} (M : ComputableTLAPlus.Memory V) (F : FIFOs V) (l : Option String) : mem (M, F, l) = M

@[simp]

theorem GuardedPlusCal.LocalState.fifos_mk {V : Type u} (M : ComputableTLAPlus.Memory V) (F : FIFOs V) (l : Option String) : fifos (M, F, l) = F

@[simp]

theorem GuardedPlusCal.LocalState.label_mk {V : Type u} (M : ComputableTLAPlus.Memory V) (F : FIFOs V) (l : Option String) : label (M, F, l) = l

@[simp]

theorem GuardedPlusCal.LocalState.mk_mem_fifos_label {V : Type u} (σ : LocalState V) : (σ.mem, σ.fifos, σ.label) = σ

inductive GuardedPlusCal.EvalStep {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (M : ComputableTLAPlus.Memory V) : String ⊕ ComputablePlusCal.Expression → ComputableTLAPlus.PathStep V → Prop

Resolving one segment of a reference's access path against a memory: a field segment resolves to itself, an index expression to whatever it evaluates to.

• field {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {M : ComputableTLAPlus.Memory V} (f : String) : EvalStep Ξ Ω M (Sum.inl f) (Sum.inl f)
• index {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {M : ComputableTLAPlus.Memory V} {e : ComputablePlusCal.Expression} {v : V} : ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M e v → EvalStep Ξ Ω M (Sum.inr e) (Sum.inr v)

def GuardedPlusCal.Ref.pathAborts {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (M : ComputableTLAPlus.Memory V) (r : ComputableGuardedPlusCal.Ref) : Prop

Some index expression in a reference's access path has no value. Field segments cannot fail, so only the .inr ones are considered.

Equations

• GuardedPlusCal.Ref.pathAborts Ξ Ω M r = ∃ e ∈ List.filterMap Sum.getRight? r.args, ComputableTLAPlus.ExprSemantics.Aborts Ξ Ω M e

Reduction of statements

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

Equations

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

def GuardedPlusCal.Statement.reducing.test {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (e : ComputablePlusCal.Expression) (v : V) : Set (LocalState V × Trace V × 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 GuardedPlusCal.Statement.reducing.idle {V : Type u} : Set (LocalState V × Trace V × LocalState V)

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

Equations

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

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

Equations

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

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

No statement can diverge: every constructor of Statement is a single step. Divergence only enters at the block and process levels.

Equations

• GuardedPlusCal.Statement.diverging x✝ = ∅

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

The states from which a guard-class statement is blocked — enabled by nothing yet, as opposed to going wrong. Three cases: await on a boolean that is not TRUE, with x ∈ e on a (present but) empty set, and receive on a channel that resolves to an empty FIFO. Every execution statement blocks nowhere. The trace is 1: a blocked guard emits nothing.

Equations

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

Reduction of blocks

Generic over the index family and the state type: a block reduces by composing its elements' relations left to right, and aborts (or diverges) if any prefix reduces to a state from which the next element does. Nothing here mentions values, so these definitions are reused verbatim for NetworkPlusCal.

def GuardedPlusCal.Block.listReducing {α : Bool → Type} {β : Type u_1} {γ : Type u_2} [Monoid γ] (f : ⦃b : Bool⦄ → α b → Set (β × γ × β)) (A : List (α false)) : Set (β × γ × β)

A possibly-empty list of statements as a relation. The one recursion in this section: a block is this fold over its begin, composed with its last, and every equation about a block is a list equation underneath.

A Block is non-empty by construction while a pass can hand back an empty run of statements (Guarded2Network's consumption assignments, for a branch that receives nothing), so the list form has to exist in its own right — and being homogeneous in the guard index, it cannot express a block's possibly-terminal last. That is the whole difference between the two.

foldr, not foldl: every proof about one of these is an induction on the list.

Equations

• GuardedPlusCal.Block.listReducing f A = List.foldr (fun (x1 : α false) (x2 : Set (β × γ × β)) => f x1 ∘ᵣ₂ x2) Relation.Idle A

def GuardedPlusCal.Block.listAborting {α : Bool → Type} {β : Type u_1} {γ : Type u_2} [Monoid γ] (g : ⦃b : Bool⦄ → α b → Set (β × γ)) (f : ⦃b : Bool⦄ → α b → Set (β × γ × β)) (A : List (α false)) : Set (β × γ)

The list counterpart of Block.aborting — and of Block.diverging too. Those two are the same function, so this one serves both, at whichever instantiation the caller passes (Block.diverging_prepend is what states it under the diverging name).

Equations

• GuardedPlusCal.Block.listAborting g f A = List.foldr (fun (S : α false) (sem : Set (β × γ)) => g S ∪ f S ∘ᵣ₁ sem) ∅ A

def GuardedPlusCal.Block.reducing {α : Bool → Type} {β : Type u_1} {γ : Type u_2} [Monoid γ] {b : Bool} (f : ⦃b : Bool⦄ → α b → Set (β × γ × β)) (B : Block α b) : Set (β × γ × β)

A block's begin run as a list, then its last. Not a recursion of its own: Block.reducing and Block.listReducing computed the same fold before, differing only in that a block's last statement may be terminal, and keeping two recursions meant every equation had to be proved twice and bridged.

Equations

• GuardedPlusCal.Block.reducing f B = GuardedPlusCal.Block.listReducing f B.begin ∘ᵣ₂ f B.last

def GuardedPlusCal.Block.aborting {α : Bool → Type} {β : Type u_1} {γ : Type u_2} [Monoid γ] {b : Bool} (f : ⦃b : Bool⦄ → α b → Set (β × γ)) (g : ⦃b : Bool⦄ → α b → Set (β × γ × β)) (B : Block α b) : Set (β × γ)

A block's begin run as a list, then its last. Not a recursion of its own: Block.reducing and Block.listReducing computed the same fold before, differing only in that a block's last statement may be terminal, and keeping two recursions meant every equation had to be proved twice and bridged.

Equations

• GuardedPlusCal.Block.aborting f g B = GuardedPlusCal.Block.listAborting f g B.begin ∪ GuardedPlusCal.Block.listReducing g B.begin ∘ᵣ₁ f B.last

def GuardedPlusCal.Block.diverging {α : Bool → Type} {β : Type u_1} {γ : Type u_2} [Monoid γ] {b : Bool} (f : ⦃b : Bool⦄ → α b → Set (β × γ)) (g : ⦃b : Bool⦄ → α b → Set (β × γ × β)) (B : Block α b) : Set (β × γ)

A block's begin run as a list, then its last. Not a recursion of its own: Block.reducing and Block.listReducing computed the same fold before, differing only in that a block's last statement may be terminal, and keeping two recursions meant every equation had to be proved twice and bridged.

Equations

• GuardedPlusCal.Block.diverging f g B = GuardedPlusCal.Block.listAborting f g B.begin ∪ GuardedPlusCal.Block.listReducing g B.begin ∘ᵣ₁ f B.last

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

Reduction of atomic branches

A branch is its precondition followed by its action. A branch with no precondition is the action alone, which is why the missing case composes with the identity relation rather than with ∅.

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

Equations

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

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

Equations

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

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

Equations

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

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

The states from which an atomic branch is blocked: its precondition reduces to a state at which some later guard blocks. A branch with no precondition — a bare action — blocks nowhere, since an execution statement never blocks.

Equations

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