The process and algorithm layers.

Nothing here mentions either language's AST. A thread has no denotation of its own — it only owns labels — and a process is scheduled entirely by label, so the whole layer is parameterized by one thing: a code table saying what the block at each label does. A label the process does not own is simply absent from its table, mapping to ∅ in both components, so nothing downstream needs a separate notion of ownership to know a label is unschedulable. Both GuardedPlusCal and NetworkPlusCal build their table from their own syntax and instantiate what follows; NetworkPlusCal's table additionally fills relay with its .rx threads' label-free receiving steps, which is the only way the two languages differ at this level.

Instances/AlgState are indexed by an arbitrary ι rather than by a Process value. The paper writes the algorithm state as a set of pairs ⟨P, σ⟩ and updates it with Ps \ {⟨P,σ⟩} ∪ {⟨P,σ'⟩}, which needs P only as a name to pair the state with. Algebra itself is not generic: both languages index a process instance by its declaring Process's own name paired with the identity it runs under, so ι = String × V at every use, and a compiled algorithm's code table is exactly the function String × V → CodeTable V that reads.

The three algorithm-level semantics are closed forms over the algorithm step — step*, step* ∘ᵣ₁ immediateAbort, step^∞ — rather than fixed points of endofunctions. The refinement framework proves one preservation law per operator (VerifiedCompiler/Denotational/ StrongRefinement.lean), so nothing downstream has to unfold a fixed point; the identities with the corresponding least fixed points are in VerifiedCompiler/ClosedForm.lean, as checks.

@[reducible, inline]

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

A process state: the process's local memory together with the set of labels currently scheduled for execution — at most one per thread, though nothing here enforces that. The paper's PState = (Var → Value) × 𝒫(Labels).

Equations

• GuardedPlusCal.ProcState V = (ComputableTLAPlus.Memory V × Set String)

@[reducible, inline]

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

A process's full state, including the channels it can see. Channels are global, so the algorithm layer threads one copy through every process rather than giving each its own.

Equations

• GuardedPlusCal.ProcConfig V = (GuardedPlusCal.ProcState V × GuardedPlusCal.FIFOs V)

structure GuardedPlusCal.CodeTable (V : Type u) : Type u

The paper's Ξₚ: what the atomic block at each label does, together with any step the process takes with no label scheduled. reducing/aborting are keyed by label — a block can step or go wrong, and there is no third, since a block never diverges (its non-terminating semantics is empty, every statement being a single step). relay collects the label-free steps.

A label with no block maps to ∅ in reducing/aborting, which makes it unschedulable rather than an error. blocking at such a label is univ instead — vacuously blocked — and owned is what a consumer intersects the scheduled set against to tell a blocked process from a done one.

• reducing : String → Set (LocalState V × Trace V × LocalState V)

  Where the block at this label can step to, and what it emits.

• aborting : String → Set (LocalState V × Trace V)

  Where the block at this label goes wrong.

• relay : Set (LocalState V × Trace V × LocalState V)

  Reducing steps taken with no scheduled label consumed and none produced — a .rx thread's receiving steps. Empty for a process with no such thread.

• blocking : String → Set (LocalState V × Trace V)

  Where the block at this label is blocked — every one of its branches waiting on a guard. univ at a label the process does not own, which owned and procBlocking gate out.

• owned : Set String

  The labels the process's code blocks carry — the paper's ⋃ Labels(Tᵢ). A scheduled label outside this set is a sentinel like Done, not a block to wait on.

• relayBlocking : Set (LocalState V)

  States in which every one of the process's relay threads is itself blocked — its channel resolves to an empty FIFO. univ for a process with no such thread.

Processes

def GuardedPlusCal.CodeTable.procReducing {V : Type u} (T : CodeTable V) (self : V) : Set (ProcConfig V × Trace V × ProcConfig V)

One step of a process: either pick a scheduled label the process owns, run the block at that label, and replace the label with the one the block's terminal goto reached; or take one of the process's label-free relay steps, leaving the scheduled set untouched.

A relay step is available only while the process still owns a scheduled label — (L ∩ T.owned) non-empty, the same "not done" condition procBlocking gates on. This is the paper's L ≠ {Done} side condition on receive: a .rx thread stops relaying once every code thread has reached its sentinel, so a finished process contributes no further steps rather than looping on its mailbox forever.

self is the process instance's identity. The paper's self ↦ p ∈ M side condition appears here as a lookup: a process only steps in a memory that binds its own identity, which initProc establishes and no step disturbs.

Equations

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

def GuardedPlusCal.CodeTable.procAborting {V : Type u} (T : CodeTable V) (self : V) : Set (ProcConfig V × Trace V)

A process goes wrong when the block at one of its scheduled labels does.

Equations

• T.procAborting self = {(((M, L), F), τ) : GuardedPlusCal.ProcConfig V × GuardedPlusCal.Trace V | ∃ l ∈ L, ((M, F, none), τ) ∈ T.aborting l ∧ Finmap.lookup GuardedPlusCal.selfName M = some self}

def GuardedPlusCal.CodeTable.procDiverging {V : Type u} (_T : CodeTable V) (_self : V) : Set (ProcConfig V × Trace V)

A process never diverges in one step: its semantics is one execution of one atomic block, and an atomic block's non-terminating semantics is empty. Divergence is an algorithm-level notion, and appears below as the infinite iteration of the process step.

Equations

• _T.procDiverging _self = ∅

def GuardedPlusCal.CodeTable.procBlocking {V : Type u} (T : CodeTable V) (self : V) : Set (ProcConfig V × Trace V)

The paper's ⟦P⟧∅: the process is not done — some scheduled label names a block it owns — and every such block is blocked, and every relay thread is blocked too.

Equations

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

def GuardedPlusCal.CodeTable.procDone {V : Type u} (T : CodeTable V) : Set (ProcState V)

A process is done when no scheduled label names a block it owns — every thread has reached a sentinel like Done. The complement of procBlocking's non-emptiness clause: a deadlocked configuration is one where every process is procBlocking or procDone, with at least one of the former.

Equations

• T.procDone = {(fst, L) : GuardedPlusCal.ProcState V | L ∩ T.owned = ∅}

Algorithms

@[reducible, inline]

abbrev GuardedPlusCal.Instances (ι V : Type u) : Type u

Every process instance paired with its own state — a partial function, not the paper's set of pairs 𝒫(⟨P,σ⟩). P is only ever used as a name to pair a state with, so writing it as a set costs a soundness obligation ("at most one state per instance") for nothing: as a function the property is definitional, not carried.

Equations

• GuardedPlusCal.Instances ι V = (ι → Option (GuardedPlusCal.ProcState V))

noncomputable def GuardedPlusCal.Instances.update {V ι : Type u} (Ps : Instances ι V) (p : ι) (σ : Option (ProcState V)) : Instances ι V

Replacing one instance's state. A named wrapper around Function.update rather than raw calls to it at each site: Function.update needs [DecidableEq ι], and ι is arbitrary here, so every call would otherwise resolve its own (classically-derived) instance independently. Two proof terms built that way are propositionally but not definitionally equal, which breaks the moment one has to match the exact term Algebra.step itself produces (algRelatesTo.block_step/.rx_step's hQs hypotheses do exactly that). Naming the update pins one instance, used everywhere.

Equations

• Ps.update p σ = Function.update Ps p σ

@[simp]

theorem GuardedPlusCal.Instances.update_self {V ι : Type u} (Ps : Instances ι V) (p : ι) (σ : Option (ProcState V)) : Ps.update p σ p = σ

theorem GuardedPlusCal.Instances.update_of_ne {V ι : Type u} {Ps : Instances ι V} {p q : ι} (h : q ≠ p) (σ : Option (ProcState V)) : Ps.update p σ q = Ps q

@[reducible, inline]

abbrev GuardedPlusCal.AlgState (ι V : Type u) : Type u

An algorithm state: every process instance paired with its own state, plus the shared channels.

Equations

• GuardedPlusCal.AlgState ι V = (GuardedPlusCal.Instances ι V × GuardedPlusCal.FIFOs V)

@[reducible, inline]

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

Everything the algorithm layer needs to know about its processes: what the block at each label does. A process instance's identity is read off its own index — self, the paper's P*_red side condition, is p.2 throughout, since ι = String × V pairs a declaring Process's name with the specific identity it runs under.

Equations

• GuardedPlusCal.Algebra V = (String × V → GuardedPlusCal.CodeTable V)

def GuardedPlusCal.Algebra.step {V : Type u} (A : Algebra V) : Set (AlgState (String × V) V × Trace V × AlgState (String × V) V)

The paper's P*_red: one step of one process, chosen non-deterministically, with every other process and the channels carried through.

Equations

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

def GuardedPlusCal.Algebra.immediateAbort {V : Type u} (A : Algebra V) : Set (AlgState (String × V) V × Trace V)

Some process goes wrong now: the immediate half of the aborting semantics, with no steps taken first. Named on its own because the aborting semantics is built from it by composition rather than by iterating a functional that mentions it.

Equations

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

def GuardedPlusCal.Algebra.immediateBlock {V : Type u} (A : Algebra V) : Set (AlgState (String × V) V × Trace V)

The algorithm is deadlocked now: the immediate half of the blocking semantics. Every process is procBlocking or procDone, and at least one is procBlocking — a process finishing while another wedges is still a deadlock (the finished one just cannot help). ∀/∃ where immediateAbort is a plain ∃, because one process going wrong stops the algorithm but a deadlock needs nothing to be able to move.

Equations

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

def GuardedPlusCal.Algebra.reducing {V : Type u} (A : Algebra V) : Set (AlgState (String × V) V × Trace V × AlgState (String × V) V)

Every finite sequence of algorithm steps, with the concatenated trace: step*.

Given directly rather than as μX. Id ∪ X ∘ᵣ₂ step, for the same reason as Algebra.diverging and Algebra.aborting — all three semantics are the closed forms the refinement framework's operator-preservation lemmas are stated at, so no proof has to unfold a fixed point before it can say anything. The empty execution is Relation.star.refl, not a disjunct to be supplied. VerifiedCompiler/ClosedForm.lean carries the identity with the least fixed point.

Equations

• A.reducing = Relation.star A.step

def GuardedPlusCal.Algebra.aborting {V : Type u} (A : Algebra V) : Set (AlgState (String × V) V × Trace V)

Every finite sequence of steps ending in a process going wrong: step* ∘ᵣ₁ immediateAbort.

Equations

• A.aborting = Relation.star A.step ∘ᵣ₁ A.immediateAbort

def GuardedPlusCal.Algebra.blocking {V : Type u} (A : Algebra V) : Set (AlgState (String × V) V × Trace V)

Every finite sequence of steps ending in the whole config blocked: step* ∘ᵣ₁ immediateBlock. Parallel to Algebra.aborting; the reducing prefix is Relation.star A.step unrestricted.

Equations

• A.blocking = Relation.star A.step ∘ᵣ₁ A.immediateBlock

def GuardedPlusCal.Algebra.diverging {V : Type u} (A : Algebra V) : Set (AlgState (String × V) V × Trace V)

Every infinite sequence of steps, each execution paired with the infinite product of the traces its steps emit.

Not the greatest fixed point of X ↦ step ∘ᵣ₁ X. That functional is not contractive when a step can emit the empty trace: at step = {(σ, 1, σ)} it is the identity, whose greatest fixed point is ⊤ — every trace whatsoever paired with σ, rather than the 1 that execution actually emits. Silent steps are not a corner case here, since Behavior observes only print/send and so while TRUE { x := x + 1 } is an infinite chain of them. Relation.omega takes the product of what the steps emit and gets this right by construction.

The two agree exactly when Relation.Productive step holds, which Algebra.step does not satisfy; Relation.gfp_eq_closedForm states that boundary.

Equations

• A.diverging = Relation.omega A.step

def GuardedPlusCal.Algebra.isDone {V : Type u} (A : Algebra V) (σ : AlgState (String × V) V) : Prop

A configuration in which every process instance has finished — no scheduled label names a block it still owns (CodeTable.procDone). The paper's isDone.

Equations

• A.isDone σ = ∀ (p : String × V) (τ : GuardedPlusCal.ProcState V), σ.1 p = some τ → τ ∈ (A p).procDone

def GuardedPlusCal.Algebra.terminating {V : Type u} (A : Algebra V) : Set (AlgState (String × V) V × Trace V × AlgState (String × V) V)

The paper's ⟦A⟧⁺, bar the init restriction (Compiler.Correctness carries the initial states as its own coverage conjunct rather than in the sets — see VerifiedCompiler/Denotational/Correctness.lean).

Algebra.reducing on its own is a reachability relation — every partial run to any configuration, so it overlaps Algebra.blocking at the endpoint and holds every finite prefix of a divergent run. The isDone on the endpoint is what makes this the terminating semantics: a complete execution that has actually run to completion.

Equations

• A.terminating = {x : GuardedPlusCal.AlgState (String × V) V × GuardedPlusCal.Trace V × GuardedPlusCal.AlgState (String × V) V | x ∈ A.reducing ∧ A.isDone x.2.2}

The initial-state relation

init is a relation, not a function: a process's local variables are given by initializer expressions and evaluation is relational (ExprSemantics.Eval), so an algorithm with a meaningless initializer has no initial state rather than a junk one. Compiler.Correctness uses it to state that every initial state of the compiled algorithm is covered by a related initial state of the source; the four semantics above are not themselves restricted to it.

def GuardedPlusCal.InitMem {V : Type u} [ComputableTLAPlus.ExprSemantics V] (inits : List (String × ComputablePlusCal.Expression)) (vs : List V) (M : ComputableTLAPlus.Memory V) : ComputableTLAPlus.Memory V

The memory a list of initializers and their values builds on top of a memory already in hand: each declared name bound to its own value, in declaration order, so a name declared twice keeps the later binding. Named rather than written inline in InitProc below, so that extending an initializer list is a statement about this function alone.

Equations

• GuardedPlusCal.InitMem inits vs M = List.foldl (fun (M : ComputableTLAPlus.Memory V) (xv : String × V) => Finmap.insert xv.1 xv.2 M) M ((List.map Prod.fst inits).zip vs)

def GuardedPlusCal.InitProc {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (self : V) (inits : List (String × ComputablePlusCal.Expression)) (entry : Set String) (σ : ProcState V) : Prop

InitProc self inits σ — σ is a valid initial state for a process instance with identity self, local variable initializers inits, and initial label set entry.

Equations

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

theorem GuardedPlusCal.InitProc.labels {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {self : V} {inits : List (String × ComputablePlusCal.Expression)} {entry : Set String} {σ : ProcState V} (h : InitProc Ξ Ω self inits entry σ) : σ.2 = entry

An initial state starts at the entry labels, and nothing else. The one projection of InitProc that needs no work, named so that reading it does not cost an obtain of the whole existential.

theorem GuardedPlusCal.eval_forall₂_inj {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {M : ComputableTLAPlus.Memory V} {inits : List (String × ComputablePlusCal.Expression)} {vs ws : List V} (h : List.Forall₂ (fun (ie : String × ComputableTLAPlus.Expression ComputableTLAPlus.Typ) (v : V) => ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M ie.2 v) inits vs) (h' : List.Forall₂ (fun (ie : String × ComputableTLAPlus.Expression ComputableTLAPlus.Typ) (v : V) => ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M ie.2 v) inits ws) : vs = ws

A list of expressions evaluates to at most one list of values — ExprSemantics.evalUnique pointwise.

theorem GuardedPlusCal.InitProc.inj {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {self : V} {inits : List (String × ComputablePlusCal.Expression)} {entry : Set String} {σ σ' : ProcState V} (h : InitProc Ξ Ω self inits entry σ) (h' : InitProc Ξ Ω self inits entry σ') : σ = σ'

An instance has at most one initial state. Everything InitProc fixes is fixed: the label set is entry outright, and the memory is a fold over the initializers' values, which ExprSemantics.evalUnique pins one by one.

This is what makes Algorithm.init well-defined as a characterization of a function Ps: the right-hand side of its ↔ pins at most one σ per instance, InitMem.inj and this lemma being why.

theorem GuardedPlusCal.InitMem.append {V : Type u} [ComputableTLAPlus.ExprSemantics V] {is₁ is₂ : List (String × ComputablePlusCal.Expression)} {ws₁ ws₂ : List V} {M : ComputableTLAPlus.Memory V} (hlen : is₁.length = ws₁.length) : InitMem (is₁ ++ is₂) (ws₁ ++ ws₂) M = InitMem is₂ ws₂ (InitMem is₁ ws₁ M)

InitMem over an appended list is one fold on top of the other, provided the values split where the names do. The equation the two InitProc.append lemmas below share.

theorem GuardedPlusCal.InitMem.lookup_ne {V : Type u} [ComputableTLAPlus.ExprSemantics V] {inits : List (String × ComputablePlusCal.Expression)} {ws : List V} {x y : String} {M : ComputableTLAPlus.Memory V} (hname : ∀ e ∈ inits, e.1 = y) (hxy : x ≠ y) : Finmap.lookup x (InitMem inits ws M) = Finmap.lookup x M

Initializers all declaring one name touch only that name. Every write the fold makes is at y, so a lookup anywhere else reads straight through to the memory the fold started from.

theorem GuardedPlusCal.InitMem.lookup_mem {V : Type u} [ComputableTLAPlus.ExprSemantics V] {inits : List (String × ComputablePlusCal.Expression)} {ws : List V} {y : String} {M : ComputableTLAPlus.Memory V} (hname : ∀ e ∈ inits, e.1 = y) (hne : inits ≠ []) (hlen : inits.length = ws.length) : ∃ v ∈ ws, Finmap.lookup y (InitMem inits ws M) = some v

And a non-empty such list leaves that name bound to one of their values. Which one is the last, but no caller needs to know that — what they need is that the value is one of those the initializers evaluated to, so that a property shared by all of them holds of it.

theorem GuardedPlusCal.InitProc.append {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {self : V} {is₁ is₂ : List (String × ComputablePlusCal.Expression)} {e₁ e₂ : Set String} {σ' : ProcState V} (h : InitProc Ξ Ω self (is₁ ++ is₂) e₂ σ') : ∃ (M : ComputableTLAPlus.Memory V) (ws : List V), InitProc Ξ Ω self is₁ e₁ (M, e₁) ∧ List.Forall₂ (fun (ie : String × ComputableTLAPlus.Expression ComputableTLAPlus.Typ) (v : V) => ComputableTLAPlus.ExprSemantics.Eval Ξ Ω (Finmap.singleton selfName self) ie.2 v) is₂ ws ∧ σ'.1 = InitMem is₂ ws M

A state over a longer initializer list is one over the shorter, written on top of. Every initializer is evaluated under the same memory — self alone, never the one being accumulated — so appending to the list neither disturbs the values already taken nor makes new ones depend on them, and the fold splits where the list does. The shorter state's label set is free, being whatever the caller's own init asks for.

theorem GuardedPlusCal.InitProc.append_of {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {self : V} {is₁ is₂ : List (String × ComputablePlusCal.Expression)} {e₁ e₂ : Set String} {σ : ProcState V} {ws : List V} (h : InitProc Ξ Ω self is₁ e₁ σ) (hws : List.Forall₂ (fun (ie : String × ComputableTLAPlus.Expression ComputableTLAPlus.Typ) (v : V) => ComputableTLAPlus.ExprSemantics.Eval Ξ Ω (Finmap.singleton selfName self) ie.2 v) is₂ ws) : InitProc Ξ Ω self (is₁ ++ is₂) e₂ (InitMem is₂ ws σ.1, e₂)

The converse: values for the added initializers build a state over the longer list. The existence direction — an initial state over the shorter list extends to one over the longer.

Instantiating for Guarded PlusCal

Every GuardedPlusCal.Thread is a plain List AtomicBlock, so a process owns exactly its blocks' labels and a label denotes the union of its block's branches. NetworkPlusCal has its own instantiation, differing only in that a .rx thread contributes one more label (Core/NetworkPlusCal/Semantics/Process.lean).

def GuardedPlusCal.Process.ownedLabels (p : ComputableGuardedPlusCal.Process) : Set String

Every label a process owns, across all of its threads.

Equations

• GuardedPlusCal.Process.ownedLabels p = {l : String | ∃ T ∈ p.threads, ∃ B ∈ T, B.label = l}

def GuardedPlusCal.Process.entryLabels (p : ComputableGuardedPlusCal.Process) : Set String

The label each thread starts at: the first block in program order. A thread with no blocks contributes nothing and is simply never scheduled.

Equations

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

theorem GuardedPlusCal.Process.entryLabels_subset_ownedLabels {p : ComputableGuardedPlusCal.Process} : entryLabels p ⊆ ownedLabels p

A thread's first block is one of its blocks, so a process starts at labels it owns.

def GuardedPlusCal.Process.codeTable {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (p : ComputableGuardedPlusCal.Process) : CodeTable V

The paper's Ξₚ: a label denotes the union of its block's branches. A label the process does not own denotes ∅ in both components, making it unschedulable.

Equations

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

Instantiating the algorithm layer

Processes are indexed by String × V — the declaring Process's own name together with a specific instance's identity. Algebra's answer does not depend on which instance, only on the Process the name resolves to, so it looks the name up and answers from that Process's own codeTable; a name with no matching Process (unreachable for any state an actual Algorithm.init ever produces) answers with the empty table, same "absent label is just unschedulable" convention codeTable itself already uses.

def GuardedPlusCal.Algorithm.algebra {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (algo : ComputableGuardedPlusCal.Algorithm) : Algebra V

Assembles a whole Algorithm's Algebra, per the module doc above.

Equations

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

def GuardedPlusCal.identitiesOf {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (shape : Bool) (id : ComputablePlusCal.Expression) : Set V

The instance identities an «=|∈»/id pair contributes: id's own value for =, each member of id's (set) value for ∈. Evaluated under the empty memory — WellFormedness/Restrictions.lean bans a process from referencing any module-level VARIABLE, so id can only mention CONSTANTs and literals, and there is nothing else to evaluate it against.

Stated about the two fields rather than about a process so that NetworkPlusCal can share it: the two languages' Process.identities are then the same function of the same two fields, and a pass that preserves them preserves the instances by rewriting, with no unfolding downstream.

Equations

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

def GuardedPlusCal.Process.identities {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (p : ComputableGuardedPlusCal.Process) : Set V

The instance identities an «=|∈»/id pair contributes: id's own value for =, each member of id's (set) value for ∈. Evaluated under the empty memory — WellFormedness/Restrictions.lean bans a process from referencing any module-level VARIABLE, so id can only mention CONSTANTs and literals, and there is nothing else to evaluate it against.

Stated about the two fields rather than about a process so that NetworkPlusCal can share it: the two languages' Process.identities are then the same function of the same two fields, and a pass that preserves them preserves the instances by rewriting, with no unfolding downstream.

Equations

• GuardedPlusCal.Process.identities Ξ Ω p = GuardedPlusCal.identitiesOf Ξ Ω p.«=|∈» p.id

theorem GuardedPlusCal.Process.identities_eq {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {p : ComputableGuardedPlusCal.Process} : identities Ξ Ω p = identitiesOf Ξ Ω p.«=|∈» p.id

Process.identities reads nothing but the two fields, so a pass preserving them preserves the instances by rewriting.

def GuardedPlusCal.initOf (v : String × ComputableTLAPlus.Typ × Bool × Option (Bool × ComputablePlusCal.Expression)) : Option (String × ComputablePlusCal.Expression)

One declared local in the shape InitProc takes it — its name paired with its initializer, and nothing when it has none. Named rather than written inline in initsOf below so that List's own filterMap lemmas apply to initsOf with no unfolding at the sites that reason about it.

Equations

• GuardedPlusCal.initOf v = Option.map (fun (x : Bool × ComputablePlusCal.Expression) => match x with | (fst, e) => (v.1, e)) v.2.2.2

def GuardedPlusCal.initsOf (vars : List (String × ComputableTLAPlus.Typ × Bool × Option (Bool × ComputablePlusCal.Expression))) : List (String × ComputablePlusCal.Expression)

A declared-locals list's initializers, in the shape InitProc takes them: the variables that have one, paired with it.

Stated about the list rather than about a process so that NetworkPlusCal can share it — the two languages' Process.inits are then the same function of the same field, which is what lets a pass that only extends the list say so.

Equations

• GuardedPlusCal.initsOf vars = List.filterMap GuardedPlusCal.initOf vars

theorem GuardedPlusCal.initsOf_eq_filterMap {vars : List (String × ComputableTLAPlus.Typ × Bool × Option (Bool × ComputablePlusCal.Expression))} : initsOf vars = List.filterMap initOf vars

A declared-locals list's initializers, in the shape InitProc takes them: the variables that have one, paired with it.

Stated about the list rather than about a process so that NetworkPlusCal can share it — the two languages' Process.inits are then the same function of the same field, which is what lets a pass that only extends the list say so.

theorem GuardedPlusCal.initsOf_append {vs ws : List (String × ComputableTLAPlus.Typ × Bool × Option (Bool × ComputablePlusCal.Expression))} : initsOf (vs ++ ws) = initsOf vs ++ initsOf ws

The initializers of an appended locals list split where the list does.

def GuardedPlusCal.Process.inits (p : ComputableGuardedPlusCal.Process) : List (String × ComputablePlusCal.Expression)

A declared-locals list's initializers, in the shape InitProc takes them: the variables that have one, paired with it.

Stated about the list rather than about a process so that NetworkPlusCal can share it — the two languages' Process.inits are then the same function of the same field, which is what lets a pass that only extends the list say so.

Equations

• GuardedPlusCal.Process.inits p = GuardedPlusCal.initsOf p.localState.variables

theorem GuardedPlusCal.Process.inits_eq {p : ComputableGuardedPlusCal.Process} : inits p = initsOf p.localState.variables

Process.inits reads nothing but the declared locals, so a pass that only extends them can say so by rewriting.

def GuardedPlusCal.Algorithm.init {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (algo : ComputableGuardedPlusCal.Algorithm) : AlgState (String × V) V → Prop

A valid initial state: every declared Process contributes exactly the instances its own «=|∈»/id calls for, each starting per InitProc at its own entry labels, and no others.

Stated as a characterization of membership rather than as "for each declared instance some state exists". The weaker reading does not constrain Ps at all — it is satisfied by an Instances that also holds junk pairs, or two states for one instance, since an existential is still witnessed. As an equation on a function, "one state per instance" is not a further clause to derive — it is what Ps i = .some σ ↔ … already says, InitProc.inj pinning the right-hand side to at most one σ.

Every declared channel/fifo starts with an empty queue at every index its own domain admits — not simply "F has no entries": Statement.reducing/.aborting's F.lookup = none case is an abort (Denotational.lean), reserved for an index outside the declared domain entirely, not for "nothing sent yet".

Equations

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