The expression layer that the PlusCal denotational semantics (Core/GuardedPlusCal/Semantics/Denotational.lean and its NetworkPlusCal counterpart) sits on top of, kept abstract.

Statement semantics genuinely need to look inside values — await/assert compare against TRUE, with x ∈ e picks a member of a set, assign/receive write into a value along a reference's path, receive applies the coercion the elaborator recorded. None of that can be written against a bare Value : Type, so every such operation is a field of ExprSemantics rather than a definition over known constructors.

Evaluation is a relation, not an Option-valued function: a user-defined operator call has to re-descend into that operator's body, jumping to an unrelated syntax tree with no measure Lean's termination checker can see. A relation needs only strict positivity, and an expression with no derivation tree is exactly an expression with no value — which is why Aborts below is derived from Eval rather than being a second parameter.

Eval also takes an OperatorEnv (Ξ) and a Model (Ω), separate from Memory — see those types' own docs — to resolve a user-defined operator's name and a CONSTANT's value; see evalVar for how the three environments interact.

Refining this to the real TLA⁺ semantics means providing one ExprSemantics instance for a concrete value type; nothing downstream of this file changes.

@[reducible, inline]

abbrev ComputableTLAPlus.OperatorEnv : Type

The operator environment: a static table from a declaring module's name and an operator name in it to that operator's formal parameters (name paired with arity — 0 for a plain value parameter, n > 0 for an n-ary higher-order parameter) and its defining body expression. Mirrors Declaration.operator's own List (String × Nat) → Expression α shape, since Ξ is populated from exactly those declarations, one module at a time.

Keyed by module name because Origin.module name — the tag a .var node referring to an operator carries, whether the operator lives in the same module or was reached through EXTENDS — already names the module to look in; evalVar below consults Ξ only for that origin, so a name can never be ambiguous between two modules'. A CONSTANT declaration is not in Ξ — it has no defining body — see Model below for how a CONSTANT's .var node gets its value instead.

Not indexed by V: unlike Memory, an unevaluated operator body is a piece of syntax, not a value, so Ξ needs no value type to be well-formed. Kept a plain function rather than a Finmap — nothing in this file's laws ever needs to enumerate or compare two Ξs, only look one name up.

Equations

• ComputableTLAPlus.OperatorEnv = (String → String → Option (List (String × ℕ) × ComputableTLAPlus.Expression ComputableTLAPlus.Typ))

def ComputableTLAPlus.OperatorEnv.WellScoped (Ξ : OperatorEnv) : Prop

Every operator body in Ξ is closed: it reads nothing from memory. evalLocal/evalSubst need this — a var_op0/opCall_op step evaluates a body (or its substParams form) that is not a subterm of the call, so agreement on the call's free variables says nothing about that body unless the body is closed. Populated Ξs satisfy it by construction: an operator definition's body is checked against a scope holding exactly its parameters (Origin.bound) plus module-level names (Origin.module), and freeVars counts neither — only Origin.free, which a body never has.

Equations

• Ξ.WellScoped = ∀ (m x : String) (params : List (String × ℕ)) (body : ComputableTLAPlus.Expression ComputableTLAPlus.Typ), Ξ m x = some (params, body) → body.freeVars = ∅

@[irreducible]

def TypedTLAPlus.Coercion.FreshFor : Coercion → Finset String → Prop

c's synthesized binder names avoid S — and, through the nested {x}/insert y S recursions, each other. The freshness side condition evalCoerce needs: Coercion.applyComputable for .seqToFun and .function wraps the coerced expression e in a binder c introduces and re-evaluates e underneath it, so unless that binder is fresh for e the built term captures and the law is false. S is instantiated to e.freeVars at the law; a real compilation discharges it because every coercion binder is MonadFresh-minted and e's names are not.

Only .seqToFun/.function place e under a binder — the other cases keep it in domain or argument position, so their arms impose nothing on S directly and only recurse. .set/inner .function recurse against {x} rather than S because there the sub-expression is the bare binder node .var x _ .binder, not something built over e. .function also keeps its value binder y off x: applyComputable's recovered-argument CHOOSE reuses x, and the built x = y comparison is only correct when the two are distinct.

Equations

• TypedTLAPlus.Coercion.id.FreshFor x✝ = True
• TypedTLAPlus.Coercion.strToSeq.FreshFor x✝ = True
• (TypedTLAPlus.Coercion.seqToFun τ i).FreshFor x✝ = (i ∉ x✝)
• (TypedTLAPlus.Coercion.bagToFun τ i).FreshFor x✝ = (i ∉ x✝)
• (TypedTLAPlus.Coercion.tupleToSeq n τ hn).FreshFor x✝ = True
• (TypedTLAPlus.Coercion.set x_2 τ τ' c).FreshFor x✝ = c.FreshFor {x_2}
• (TypedTLAPlus.Coercion.tuple coes τs τs').FreshFor x✝ = ∀ c ∈ coes, c.FreshFor x✝
• (TypedTLAPlus.Coercion.record fields).FreshFor x✝ = ∀ f ∈ fields, f.2.1.FreshFor x✝
• (TypedTLAPlus.Coercion.function x_2 y dom rng dom' rng' cD cR).FreshFor x✝ = (y ∉ insert x_2 x✝ ∧ cD.FreshFor {x_2} ∧ cR.FreshFor (insert y x✝))
• (c₁.comp c₂).FreshFor x✝ = (c₁.FreshFor x✝ ∧ c₂.FreshFor x✝)

theorem TypedTLAPlus.Coercion.FreshFor.mono {c : Coercion} {S S' : Finset String} : c.FreshFor S → S' ⊆ S → c.FreshFor S'

FreshFor is antitone in the avoided set: fewer names to dodge is a weaker demand. Lets a recursive evalCoerce call at a sub-expression whose free variables have shrunk (they only ever shrink — Coercion.applyComputable adds no free variable) reuse the parent's hypothesis.

@[reducible, inline]

abbrev ComputableTLAPlus.Model (V : Type u) : Type u

The model: an assignment of a value to every CONSTANT a run fixes one for, keyed the same way Ξ is (declaring module, then name) since a CONSTANT's .var node carries the same Origin.module tag an operator reference does. Kept opaque and partial rather than computed: a CONSTANT has no defining expression to evaluate (Declaration.constants carries only a name and a type), so its value can only ever come from outside — one run's choice of Model, not this file's laws. A name with no entry has no value under Eval, same as any other partiality in this class.

Equations

• ComputableTLAPlus.Model V = (String → String → Option V)

@[reducible, inline]

abbrev ComputableTLAPlus.Memory (V : Type u) : Type u

A memory: a partial map from names to values.

Finmap, not AList. An AList is a list, so its identity includes the order its keys were inserted in — and evalLocal says evaluation depends on a memory only through lookup, so that order is information the semantics provably cannot observe. Keeping it visible makes false goals: binding two distinct names in the two possible orders gives equal lookups but unequal ALists, and any lemma commuting one write past another (Guarded2Network/Lemmas/Reorder.lean) then cannot be stated as an equation at all. Finmap is that quotient, so Finmap.insert_insert_of_ne holds and extensionality is by lookup. FIFOs is a Finmap for the same reason.

Equations

• ComputableTLAPlus.Memory V = Finmap fun (x : String) => V

@[reducible, inline]

abbrev ComputableTLAPlus.PathStep (V : Type u) : Type u

One resolved segment of a reference's access path. Mirrors ElaboratedPlusCal.Ref.args's List (String ⊕ ε) with the index expressions already evaluated: .inl f is the record field f, .inr v is the index v.

Equations

• ComputableTLAPlus.PathStep V = (String ⊕ V)

inductive ComputableTLAPlus.ResolvesPath {V : Type u} (Eval : Memory V → Expression Typ → V → Prop) (M : Memory V) : List (String ⊕ Expression Typ) → List (PathStep V) → Prop

ResolvesPath Eval M path resolved — every .inr index expression in the syntactic path path evaluates (under Eval/M) to the matching entry of the semantic path resolved; every .inl field segment carries over unchanged. What evalExcept needs to relate Expression.except's syntactic update path to updatePath's semantic one. Takes Eval as a plain parameter rather than an ExprSemantics instance so it can be stated before the class whose field it appears in.

• nil {V : Type u} {Eval : Memory V → Expression Typ → V → Prop} {M : Memory V} : ResolvesPath Eval M [] []
• inl {V : Type u} {Eval : Memory V → Expression Typ → V → Prop} {M : Memory V} {f : String} {path : List (String ⊕ Expression Typ)} {resolved : List (PathStep V)} : ResolvesPath Eval M path resolved → ResolvesPath Eval M (Sum.inl f :: path) (Sum.inl f :: resolved)
• inr {V : Type u} {Eval : Memory V → Expression Typ → V → Prop} {M : Memory V} {e : Expression Typ} {v : V} {path : List (String ⊕ Expression Typ)} {resolved : List (PathStep V)} : Eval M e v → ResolvesPath Eval M path resolved → ResolvesPath Eval M (Sum.inr e :: path) (Sum.inr v :: resolved)

class ComputableTLAPlus.ExprSemantics (V : Type u) : Type u

Everything the PlusCal semantics needs to know about expressions and the values they denote. Held abstract here; a concrete TLA⁺ evaluator later supplies one instance.

• decEq : DecidableEq V

  Values are compared for equality when used as FIFO index keys.

• Eval : OperatorEnv → Model V → Memory V → Expression Typ → V → Prop

  Eval Ξ Ω M e v — under operator environment Ξ, model Ω, and memory M, expression e denotes v. Relational rather than functional, see this file's module doc.

• tru : V

  The value of TRUE.

• isBool : V → Prop

  The value is a boolean. Only needed to state that a non-boolean guard aborts, as opposed to merely blocking.

• isSet : V → Prop

  The value is a set. Same role for with x ∈ e: an empty set blocks, a non-set aborts, and mem alone cannot tell the two apart.

• mem : V → V → Prop

  mem v S — v is a member of the set value S.

• updatePath : V → List (PathStep V) → V → Option V

  updatePath old path v — old with the position named by path overwritten by v, or none when path does not resolve inside old. path = [] overwrites old outright.

• updatePath_nil {old v : V} : updatePath old [] v = some v

  The empty path overwrites the old value outright, and always succeeds. A law rather than only a remark on updatePath above, because Memory.update routes an unindexed assignment (x := e, where the reference has no .args) through updatePath too: without this, the memory such an assignment produces is not pinned to M.insert x v, and no reorder lemma can identify it with the memory substitution describes.

• seqAppend : V → V → Option V

  seqAppend s v — s with v appended on the right, none when s is not a sequence value. TLA⁺'s Append(s, v). Needed by NetworkPlusCal.Thread.rx, which drains a channel into a process-local sequence.

• isSeq : V → List V → Prop

  isSeq s vs — s is the sequence value whose elements are vs, in order. The link between the value world and a List V: a sequence-valued local and a FIFO's contents are otherwise two unrelated things, and nothing else in this class bridges them.

  A relation rather than a partial function to a list, for the same reason Eval is one: it is a fact about a value, not a computation, and a value that is not a sequence is simply related to no list. Kept element-level (no isSeq-vs-seqAppend well-formedness field): seqAppend_isSeq below is the only interaction the semantics needs.

• isSeq_inj {s : V} {vs ws : List V} : isSeq s vs → isSeq s ws → vs = ws

  A value is the sequence of at most one element list.

• eval_seq_nil {Ξ : OperatorEnv} {Ω : Model V} {M : Memory V} {τ : Typ} : ∃ (s : V), Eval Ξ Ω M (Expression.seq [] τ) s ∧ isSeq s []

  The empty sequence literal has a value, and it is the empty sequence. The one place a value has to be known to be a sequence from the syntax that produced it rather than from an operation on another sequence: seqAppend covers every step after the first, and this covers the first.

  Stated as existence for the reason seqAppend_isSeq is: totality is then part of the law. An initial state exists only if every declared initializer evaluates, so an implication would leave a <<>> initializer free to have no value at all. The implication form is isSeq_of_eval_seq_nil below, evalUnique away.

• seqAppend_isSeq {s v : V} {vs : List V} : isSeq s vs → ∃ (s' : V), seqAppend s v = some s' ∧ isSeq s' (vs ++ [v])

  Appending to a sequence value always succeeds, and appends to its element list. Stated as existence rather than as an equation on a given result so that seqAppend's totality on sequences is part of the law — Thread.rxBranch treats a failed append as an abort, which must not be reachable when inbox really holds a sequence.

• isSeq_tail {s v : V} {vs : List V} : isSeq s (v :: vs) → ∃ (t : V), isSeq t vs

  Every tail of a sequence is itself a sequence value. The counterpart of seqAppend_isSeq on the other side: that one says the value world is closed under adding an element, this one that it is closed under dropping the first. Needed because isSeq is a relation — without it a list could have no value representing it, and a compiled inbox := Tail(inbox) would be free to abort where the source it compiles does not.

• coerce : TypedTLAPlus.Coercion → V → V → Prop

  coerce c v v' — applying the coercion c to v yields v'. The value-level counterpart of Coercion.apply/Coercion.applyComputable, which act on expressions.

• evalUnique {Ξ : OperatorEnv} {Ω : Model V} {M : Memory V} {e : Expression Typ} {v w : V} : Eval Ξ Ω M e v → Eval Ξ Ω M e w → v = w

  An expression has at most one value. Eval is a relation because evaluation may fail to have a derivation, not because a TLA⁺ expression could denote two things — non-determinism enters the PlusCal semantics through with x ∈ S and process scheduling, never through an expression.

  Load-bearing rather than cosmetic: a Ref's index path resolves through EvalStep, so without this a channel reference could resolve to two different ChanKeys at once and no invariant could name the FIFO a receive reads. EvalStep.path_inj is that consequence.

• evalVar {Ξ : OperatorEnv} {Ω : Model V} {M : Memory V} {τ : Typ} {name : String} {v : V} : Eval Ξ Ω M (Expression.var τ (TypedTLAPlus.Origin.free name)) v ↔ Finmap.lookup name M = some v

  A variable node's meaning is dispatched on its Origin, each case denoting from exactly one of the three environments:

  • .free name — the name is Memory-keyed (a PlusCal variable, self, a statement with): M.lookup name.
  • .bound _ — a de Bruijn index. Eval only ever meets a binder body after it has been opened with a name, so a bare .bound node denotes nothing — False.
  • .intrinsic _ — a hardcoded builtin (=, /\, DOMAIN, …) has no value on its own; it only means something as the head of an opCall, which a concrete ExprSemantics instance dispatches off the builtin table directly. Bare, it denotes nothing — hence False, not a memory lookup.
  • .module m name — Naturals's Nat/Integers's Int denote their integer-set families; every other name is looked up in Ξ's entry for m (0-arity operator body, or Ω m name for a CONSTANT). Not covered here — no abstract consumer reads a .module node this way.

  Scoped to .free: Origin alone selects the case, and this is the only one every abstract consumer needs (all evalVar uses are on Memory-keyed names).

• evalCoerce {Ξ : OperatorEnv} {Ω : Model V} {M : Memory V} {c : TypedTLAPlus.Coercion} {e : Expression Typ} {v' : V} : Ξ.WellScoped → c.FreshFor e.freeVars → (Eval Ξ Ω M (c.applyComputable e) v' ↔ ∃ (v : V), Eval Ξ Ω M e v ∧ coerce c v v')

  Applying a coercion to an expression denotes the coercion applied to that expression's value. TypedTLAPlus.Coercion.applyComputable and coerce above are the expression-level and value-level views of one operation, and this is the only thing connecting them — a pass that compiles a coercion into synthesized syntax (Guarded2Network does, on a receive's consumption assignment) can relate the two only through this law.

  An ↔: the forward reading turns the target's evaluated right-hand side into the source's coerce obligation, the backward one builds the target's from the source's.

  Needs Ξ.WellScoped for the same reason evalLocal does: applyComputable for .seqToFun/.function re-evaluates e under a binder the coercion introduces, and relating that to e's value in the ambient memory is exactly evalLocal. The binder is opened at a name chosen fresh for e (locally-nameless, cofinite Eval rules), so the Coercion.FreshFor c e.freeVars argument is no longer load-bearing — kept only until its callers are cleaned up.

• evalLocal {Ξ : OperatorEnv} {Ω : Model V} {M₁ M₂ : Memory V} {e : Expression Typ} {v : V} : Ξ.WellScoped → (∀ x ∈ e.freeVars, Finmap.lookup x M₁ = Finmap.lookup x M₂) → (Eval Ξ Ω M₁ e v ↔ Eval Ξ Ω M₂ e v)

  Evaluation only depends on the free variables e actually reads — agreeing memories give agreeing results, for shared Ξ/Ω (immutable within one evaluation, see this file's module doc, so there is nothing to vary them against). Needs Ξ.WellScoped: an operator call reads its body through Ξ, and that body is not part of e, so its own free variables have to be confined to the operator's parameters for the call's freeVars to bound what memory the call depends on.

• evalSubst {Ξ : OperatorEnv} {Ω : Model V} {M : Memory V} {x : String} {e' e : Expression Typ} {v' v : V} : Ξ.WellScoped → e'.LC → Eval Ξ Ω M e' v' → (Eval Ξ Ω (Finmap.insert x v' M) e v ↔ Eval Ξ Ω M (Expression.subst x e' e) v)

  Substitution is evaluation-under-extended-memory, read backwards: binding x to e''s value and evaluating e agrees with evaluating e's x-substituted form under the original memory. Needs Ξ.WellScoped (an operator call's body is evaluated through Ξ, and only its parameters may occur free in it) and Expression.LC e' (e' is spliced under e's binders, so it must carry no dangling de Bruijn index).

• evalExcept {Ξ : OperatorEnv} {Ω : Model V} {M : Memory V} {f rhs : Expression Typ} {τ : Typ} {path : List (String ⊕ Expression Typ)} {vf vr v : V} {resolved : List (PathStep V)} : Eval Ξ Ω M f vf → ResolvesPath (Eval Ξ Ω) M path resolved → Eval Ξ Ω M rhs vr → (Eval Ξ Ω M (f.except τ [(path, rhs)]) v ↔ updatePath vf resolved vr = some v)

  [f EXCEPT ![path] = rhs] denotes updatePath applied to f's value, rhs's value, and the syntactic path resolved (ResolvesPath) against the same memory. Scoped to the one-update form — the only shape Expression.substRef ever produces.

theorem ComputableTLAPlus.ExprSemantics.isSeq_of_seqAppend {V : Type u} [ExprSemantics V] {s v s' : V} {vs : List V} (h : isSeq s vs) (h' : seqAppend s v = some s') : isSeq s' (vs ++ [v])

seqAppend_isSeq read against a result already in hand: seqAppend is a function, so its some result is the one the law produces.

theorem ComputableTLAPlus.ExprSemantics.isSeq_of_eval_seq_nil {V : Type u} [ExprSemantics V] {Ξ : OperatorEnv} {Ω : Model V} {M : Memory V} {τ : Typ} {s : V} (h : Eval Ξ Ω M (Expression.seq [] τ) s) : isSeq s []

eval_seq_nil read against a value already in hand: evaluation is deterministic, so the value of <<>> is the empty sequence.

def ComputableTLAPlus.ExprSemantics.Aborts {V : Type u} [ExprSemantics V] (Ξ : OperatorEnv) (Ω : Model V) (M : Memory V) (e : Expression Typ) : Prop

Aborts Ξ Ω M e — e has no value at all under Ξ/Ω/M. Derived rather than assumed: with Eval a relation, "no derivation tree" already is the meaning of "no value", so nothing links the two notions that needs stating separately.

Equations

• ComputableTLAPlus.ExprSemantics.Aborts Ξ Ω M e = ¬∃ (v : V), ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M e v

theorem ComputableTLAPlus.ExprSemantics.aborts_congr {V : Type u} [ExprSemantics V] {Ξ : OperatorEnv} {Ω : Model V} {M₁ M₂ : Memory V} {e₁ e₂ : Expression Typ} (h : ∀ (v : V), Eval Ξ Ω M₁ e₁ v ↔ Eval Ξ Ω M₂ e₂ v) : Aborts Ξ Ω M₁ e₁ ↔ Aborts Ξ Ω M₂ e₂

Aborts transported along an agreement between two evaluations. Every transfer lemma about Eval has an Aborts counterpart, and Aborts being a negated existential means each one is this same not_congr (exists_congr …) — stating it once keeps the definition's body out of the proofs that use it.

def ComputableTLAPlus.Memory.update {V : Type u} [ExprSemantics V] (M : Memory V) (x : String) (path : List (PathStep V)) (v : V) : Option (Memory V)

Memory.update M x path v — M with the position path inside x's current value overwritten by v. Fails when x is unbound, or when path does not resolve inside the value found there. Note x must already be bound: PlusCal assignment updates a declared variable, it never introduces one.

Equations

• M.update x path v = do let old ← Finmap.lookup x M let new ← ComputableTLAPlus.ExprSemantics.updatePath old path v pure (Finmap.insert x new M)

Memory.update is a two-step Option bind, and taking one apart by hand costs an unfold plus the same Option.bind_eq_*_iff rewrite every time. The two equations below are that decomposition, stated once here where the definition lives so that no proof elsewhere has to reach into the body. Both are ↔: consumers need the reading that takes a successful update apart and the one that builds a fresh update at a different memory.

theorem ComputableTLAPlus.Memory.update_eq_some_iff {V : Type u} [ExprSemantics V] {M M' : Memory V} {x : String} {path : List (PathStep V)} {v : V} : M.update x path v = some M' ↔ ∃ (old : V) (new : V), Finmap.lookup x M = some old ∧ ExprSemantics.updatePath old path v = some new ∧ M' = Finmap.insert x new M

An update succeeds exactly when the name is bound and updatePath accepts the value found there; the result is that name rebound to what came back.

theorem ComputableTLAPlus.Memory.update_eq_none_iff {V : Type u} [ExprSemantics V] {M : Memory V} {x : String} {path : List (PathStep V)} {v : V} : M.update x path v = none ↔ ∀ (old : V), Finmap.lookup x M = some old → ExprSemantics.updatePath old path v = none

An update fails exactly when the name is unbound, or updatePath rejects the value found there.

theorem ComputableTLAPlus.Memory.update_nil {V : Type u} [ExprSemantics V] {M M' : Memory V} {x : String} {v : V} (h : M.update x [] v = some M') : M' = Finmap.insert x v M

At the empty path an update is exactly insert: updatePath_nil says the old value plays no part. This is what an unindexed assignment x := e does to the memory, and it is the form substitution describes — Expression.substRef on a reference with no .args substitutes e for x outright rather than building an EXCEPT.

theorem ComputableTLAPlus.Memory.update_insert_iff {V : Type u} [ExprSemantics V] {M M₂ : Memory V} {x y : String} {path : List (PathStep V)} {u v : V} (hne : x ≠ y) : (∃ (M' : Memory V), M.update y path v = some M' ∧ M₂ = Finmap.insert x u M') ↔ update (Finmap.insert x u M) y path v = some M₂

An update and a binding of some other name commute: updating first and then binding x reaches the same memory as binding x first and then updating, and either order succeeds exactly when the other does. Memory being a Finmap is what makes this an equation rather than only a lookup-wise agreement — see that abbreviation's doc. Both readings are used, one per direction of Guarded2Network/Lemmas/Reorder.lean's with case, where the binding is the with's own.

theorem ComputableTLAPlus.ExprSemantics.evalSubstRef {V : Type u} [ExprSemantics V] {Ξ : OperatorEnv} {Ω : Model V} {M M' : Memory V} {r : ElaboratedPlusCal.Ref Typ (Expression Typ)} {rhs e : Expression Typ} {v w : V} {rpath : List (PathStep V)} (hΞ : Ξ.WellScoped) (hrhsLC : rhs.LC) (hargsLC : ∀ (eᵢ : Expression Typ), Sum.inr eᵢ ∈ r.args → eᵢ.LC) (hrhs : Eval Ξ Ω M rhs v) (hpath : ResolvesPath (Eval Ξ Ω) M r.args rpath) (hM' : M.update r.name rpath v = some M') : Eval Ξ Ω M' e w ↔ Eval Ξ Ω M (Expression.substRef r rhs e) w

evalSubst lifted from a name to a reference: evaluating in the memory an assignment produced agrees with evaluating the reference-substituted expression in the memory it started from. This is the transfer the reorder lemmas run on (Guarded2Network/Lemmas/Reorder.lean), and it is derived — evalSubst covers a bare reference directly, while a compound one needs evalVar to name the value being updated and evalExcept to say the synthesized EXCEPT denotes exactly the updatePath the assignment ran.

r's target is a declared PlusCal variable, Origin.binder, so evalVar's .module-lookup branch never applies to it — evalVar.mpr hold below goes through unconditionally, no side condition needed (see evalVar's own doc for why Origin alone, not a name-shadowing assumption, decides this).