Naming policy for Network2Go: what the generated Go calls the things a specification named, and what it calls the runtime library it links against.

Two separate concerns meet here.

• Runtime references. Generated code names the runtime library constantly, so the package qualifiers live in one place rather than being spelled at every construction site. The packages are runtime/tlaplus (TLA⁺'s own value types), runtime/comm (message passing) and runtime/locks (mutual exclusion); none of them is called runtime, deliberately, since that is Go's own package name.
• Renaming what the user wrote. Every defined name is capitalized in the generated code regardless of the original's case, except LOCAL definitions, so that definitions are exported from the package they land in. Record fields get the same treatment (a record's from/mes become From/Mes); process variables do not.

def Network2Go.tlaplusPkg : String

The runtime/tlaplus package's qualifier, as it appears in generated code.

Equations

• Network2Go.tlaplusPkg = "tlaplus"

def Network2Go.commPkg : String

The runtime/comm package's qualifier.

Equations

• Network2Go.commPkg = "comm"

def Network2Go.locksPkg : String

The runtime/locks package's qualifier.

Equations

• Network2Go.locksPkg = "locks"

def Network2Go.condlocksPkg : String

The runtime/experimental/condlocks package's qualifier — the experimental -Xgo-cond backend's Lock (which also carries a change signal) and Arbiter. Under runtime/experimental/ rather than beside runtime/locks, so nothing suggests it backs the default compilation scheme. Arbiter is what keeps generated code from ever needing sync.Once or a pointer directly: this AST has no address-of operator or pointer type, so a primitive that must not be copied has to hide behind a value-typed runtime wrapper — Lock already does this for its change signal, Arbiter does it for the one-shot arbitration a block's branches share.

Equations

• Network2Go.condlocksPkg = "condlocks"

def Network2Go.qualified (pkg name : String) : String

A qualified reference to a name in one of the runtime packages, pkg.name. Go's package qualifier is an ordinary part of the identifier as far as this AST is concerned — Go.Typ.named and Go.Expression.var both carry it as one string.

Equations

• Network2Go.qualified pkg name = toString pkg ++ toString "." ++ toString name

def Network2Go.tlaplusTyp (name : String) (args : List Go.Typ := []) : Go.Typ

A runtime type from runtime/tlaplus, applied to type arguments when generic: tlaplus.Set[τ], tlaplus.Int.

Equations

• Network2Go.tlaplusTyp name args = Go.Typ.named (Network2Go.qualified Network2Go.tlaplusPkg name) args

def Network2Go.commTyp (name : String) (args : List Go.Typ := []) : Go.Typ

A runtime type from runtime/comm: comm.Address, comm.Sender[τ].

Equations

• Network2Go.commTyp name args = Go.Typ.named (Network2Go.qualified Network2Go.commPkg name) args

def Network2Go.locksTyp (name : String) (args : List Go.Typ := []) : Go.Typ

A runtime type from runtime/locks: locks.Lock[τ].

Equations

• Network2Go.locksTyp name args = Go.Typ.named (Network2Go.qualified Network2Go.locksPkg name) args

def Network2Go.condlocksTyp (name : String) (args : List Go.Typ := []) : Go.Typ

A runtime type from runtime/experimental/condlocks: condlocks.Lock[τ], condlocks.Arbiter.

Equations

• Network2Go.condlocksTyp name args = Go.Typ.named (Network2Go.qualified Network2Go.condlocksPkg name) args

def Network2Go.tlaplusVar {α : Type} (name : String) : Go.Expression α

A reference to a runtime/tlaplus function or type-conversion, as an expression: tlaplus.MkSet, tlaplus.Bool. Applying it is Go.Expression.call, which also covers Go's conversion syntax — tlaplus.Bool(true) is a call as far as this AST is concerned.

Equations

• Network2Go.tlaplusVar name = Go.Expression.var (Network2Go.qualified Network2Go.tlaplusPkg name)

def Network2Go.commVar {α : Type} (name : String) : Go.Expression α

A reference to a runtime/comm function.

Equations

• Network2Go.commVar name = Go.Expression.var (Network2Go.qualified Network2Go.commPkg name)

def Network2Go.locksVar {α : Type} (name : String) : Go.Expression α

A reference to a runtime/locks function: locks.Acquire, locks.MkLock.

Equations

• Network2Go.locksVar name = Go.Expression.var (Network2Go.qualified Network2Go.locksPkg name)

def Network2Go.condlocksVar {α : Type} (name : String) : Go.Expression α

A reference to a runtime/experimental/condlocks function: condlocks.MkLock, condlocks.MkArbiter.

Equations

• Network2Go.condlocksVar name = Go.Expression.var (Network2Go.qualified Network2Go.condlocksPkg name)

def Network2Go.tlaplusCall {α : Type} (name : String) (args : List (Go.Expression α)) : Go.Expression α

tlaplus.f(e₁, …, eₙ).

Equations

• Network2Go.tlaplusCall name args = (Network2Go.tlaplusVar name).call args

def Network2Go.goIdent (name : String) : String

Any name from the source — user-written or compiler-synthesized — respelled as a Go identifier. Every name crossing into generated code goes through this, which is what makes the two name-spaces disjoint.

Common/Fresh.lean mints names as <prefix>$<n>, $ being chosen because a TLA⁺ identifier cannot contain one, which is what makes the scheme collision-free across passes. A Go identifier cannot contain one either — and Core/Go/Pretty.lean's sanitize will not respell it, escaping reserved words only — so the freshness argument has to be re-established in Go's alphabet rather than simply carried over.

The encoding sends _ to __ and $ to _:

source	Go
x_1 (user)	x__1
set$1 (fresh)	set_1
set_1 (user)	set__1

What carries it is parity, not the particular lengths. Every maximal run of underscores in the output is a sum of contributions, two per source _ and one per source $, so a run is odd exactly when it covers an odd number of $s. A user name contains no $ and so has only even runs; a fresh name contains exactly one and so has exactly one odd run. An odd run therefore means "compiler-introduced", and no user name can reach a fresh name's spelling however it is written.

Only the parities matter, not the lengths; leaving _ as itself is what cannot work, since that puts user underscores and $s in the same parity class.

The encoding is not injective in general and must not be reused as though it were: _$ and $_ both encode to three underscores. That costs nothing here, since telling the two name-spaces apart is all that is asked of it — but a second $ in one name would flip a run back to even and break the property silently. freshName interpolates exactly one.

Equations

• Network2Go.goIdent name = String.foldl (fun (acc : String) (c : Char) => acc ++ if (c == '_') = true then "__" else if (c == '$') = true then "_" else c.toString) "" name

def Network2Go.ordParamName (a : String) : String

The Go name of the dictionary parameter bound for a rigid type variable.

A polymorphic definition is called at many types, so its element ordering cannot be a closed expression and has to be a value parameter — the one case where ordDict reads an environment instead of building the dictionary outright. The parameter's name is derived from the type variable's rather than looked up, so that ordDict needs no environment threaded through it: the enclosing definition binds ord_a for exactly the type variables its own type mentions.

The single _ in the prefix is itself compiler-introduced, and an odd-length run, so no user name can reach it: ord_x here and a user's own ord_x (which escapes to ord__x) stay distinct.

It sits in the same shape as an escaped fresh name, so ord is reserved as a freshName prefix: freshName "ord" would mint ord$n, spelled ord_n, which is this function's answer for a type variable named n.

Equations

• Network2Go.ordParamName a = toString "ord_" ++ toString (Network2Go.goIdent a)

Renaming user-chosen names

goIdent separates the compiler's names from the user's. What is left is the user's names against each other and against Go's own vocabulary, and the requirement is that generated code never introduces shadowing.

The renaming is a pure function of the name, not a collision map, and that is forced rather than preferred. Record fields decide it: Go identifies struct types structurally, so a field name has to receive the same Go name at every occurrence or two identically-shaped records become two different Go types, and compileTyp's field sorting stops making the shapes coincide. A map would therefore have to be built from every field name in the whole program before any of it is emitted — and fields appear in inferred types, not only in declared ones, so collecting them means a pass over everything the checker produced. A pure function gives the same guarantee for free, and the same mechanism then serves definitions, so there is only one story to keep straight.

The disambiguation mark is one appended _. goIdent leaves a name's trailing underscore run even-length (or absent), so appending one makes it odd, which is the compiler's half of the parity split — a marked name is unreachable from an unmarked one however it is spelled, and from a fresh name too, those ending in a digit. The mark composes with the escaping instead of competing with it.

Which side gets marked differs by name class, and follows the conventions of the language being compiled. A definition must start uppercase to be exported and TLA⁺ definitions are conventionally already capitalized, so Init passes through and init is marked. Record fields must also be capitalized, but TLA⁺ fields are conventionally lowercase, so the marking is reversed: from becomes From, and a source From is the one marked. Each class keeps its common case clean. The two do not share a namespace — Go's struct fields are per-type, package-level names are not — so the two schemes cannot interfere.

def Network2Go.binderName (name : String) : String

The Go name of a binder: a quantifier's variable, an operator's parameter, a rigid type variable. The renaming scheme covers definitions and record fields but leaves variables alone, so this only escapes the name and steps around Go's own vocabulary.

Equations

• Network2Go.binderName name = Network2Go.avoidsReserved✝ (Network2Go.goIdent name)

def Network2Go.definitionName (isLocal : Bool) (name : String) : String

The Go name of a top-level TLA⁺ definition.

Capitalized so that the definition is exported, which is what lets generated code spread over more than one file later without revisiting the naming scheme. Uppercasing is Unicode.getUpperChar rather than String.capitalize, whose Char.toUpper is ASCII-only while the lexer accepts any Unicode letter to start an identifier (Parser_/TLAPlus.lean's identifierOrKeyword): a definition named élan becomes Élan and is exported, where an ASCII capitalize would have left it lowercase and unexported for a reason having nothing to do with the specification.

A caseless first letter has no uppercase to map to, and so stays unexported: getUpperChar is Simple_Uppercase_Mapping and leaves ß and fi alone (their full mappings are two characters, and UnicodeBasic ships no SpecialCasing.txt), while א and 日 have no uppercase in any mapping. Knowingly unhandled — TLA⁺ proper admits only ASCII identifiers, so these names are already outside the specified language and reach this function only through this parser's more permissive lexer. Everything still compiles; the definitions are merely package-local, which costs nothing while the generated code is one package.

Already-capitalized names pass through and lowercase ones are marked, so Init stays Init and init becomes Init_ — the conventional spelling of a TLA⁺ definition is the one kept clean.

LOCAL definitions must not export, so they are pushed the other way, into the lowercase-initial half, with the marking reversed to match. The two halves are disjoint by first-character case, which is what keeps a LOCAL name from colliding with an exported one. (LOCAL has no parser production today, so this arm is unreachable.)

Equations

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

def Network2Go.fieldName (name : String) : String

The Go name of a record field, renamed on the same scheme as a definition.

Marked on the opposite side from definitionName: TLA⁺ record fields are conventionally lowercase, so from becomes From, and a source From is the one that takes the mark. Package-level names and struct field names do not share a namespace, so the two schemes are free to differ.

Equations

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

Names this pass invents at package level

Compiling a process needs a Go function per atomic block, per branch, per thread and per process, plus the Network struct type — none of which the specification names. They land in the same package namespace as the compiled TLA⁺ definitions, so they have to be disjoint from those and from each other. The readable spellings are not: a scheduler called SndPi is what definitionName produces for a definition named sndPi, and a process function called Pong collides with a CONSTANT of that name. So a prefix scheme is used instead.

The shape is <Kind>_<parts…>, and the single underscore is what makes it safe. goIdent doubles every user underscore, so a single one can only come from a $ — which no user name contains. A compiler name whose first underscore is followed by more characters is therefore unreachable from any definitionName output, whose only single underscore is the trailing mark. The parts are goIdent-escaped, so distinct sources give distinct names: goIdent is injective on $-free strings, which user labels and process names are.

Every one of these is capitalized and so exported. That is deliberate for the process function — it is the entry point whoever wires the system together calls — and harmless for the rest.

def Network2Go.networkTypName : String

The Go type name for the network shape. One per compiled algorithm, not per process.

Equations

• Network2Go.networkTypName = "Net_Network"

def Network2Go.blockName (proc label : String) : String

The scheduler function for an atomic block: the Rand-driven loop over its branches.

Equations

• Network2Go.blockName proc label = toString "Blk_" ++ toString (Network2Go.goIdent proc) ++ toString "_" ++ toString (Network2Go.goIdent label)

def Network2Go.branchName (proc label : String) (i : ℕ) : String

The function for one branch of an atomic block, i counting from 1.

Equations

• Network2Go.branchName proc label i = toString "Brn_" ++ toString (Network2Go.goIdent proc) ++ toString "_" ++ toString (Network2Go.goIdent label) ++ toString "_" ++ toString i

def Network2Go.threadName (proc : String) (k : ℕ) : String

The function for a thread, k its index in the process.

Equations

• Network2Go.threadName proc k = toString "Thr_" ++ toString (Network2Go.goIdent proc) ++ toString "_" ++ toString k

def Network2Go.rxThreadName (proc : String) (k : ℕ) : String

The function for a receiving thread, k its index in the process. Kept distinct from threadName rather than sharing its numbering: the two have different signatures, and a reader should not have to count threads to tell which is which.

Equations

• Network2Go.rxThreadName proc k = toString "Rx_" ++ toString (Network2Go.goIdent proc) ++ toString "_" ++ toString k

def Network2Go.processName (proc : String) : String

The function for a whole process — the one the user calls to start it.

Equations

• Network2Go.processName proc = toString "Proc_" ++ toString (Network2Go.goIdent proc)

def Network2Go.projName (i : ℕ) : String

The Go name of tuple component i, counting from 1.

A tuple is compiled as the record shape [proj1 ↦ τ₁, …, projn ↦ τₙ], so its components are ordinary fields and get an ordinary field's capitalization. Being lowercase in the source, they land on fieldName's clean side: Proj1, not Proj1_.

Equations

• Network2Go.projName i = Network2Go.fieldName (toString "proj" ++ toString i)