Chapters 13 to 21 give the code of this book’s functionalities, protocols and games, and that code is meant to be read as a program, not as an illustration of one — a promise that has to be kept by a stated convention rather than by the reader’s good will. [5] keep exactly this promise for game-based proofs with a small, strongly typed, terminating language they call \(\mathcal {L}\), given by a context-free grammar (their Figure 15) and a short named list of the sugars they allow on top of it. This chapter takes the same two steps here: a closed grammar for what every chapter from here on calls a core — an operation’s body, already this book’s own word for it — and this book’s own short list of departures from that grammar, each named once so that every core still to come can be checked against it rather than taken on faith.
Everything before this chapter is exempt, and deliberately so. \(\opl {Guard}\), \(\opl {Silence}\) and \(\opl {Mediate}\) (Chapter 2), \(\opl {Exec}\) (Section 3.6), the dummy adversary (Section 4.4) and \(\opl {Respond}\) (Chapter 9) do not run inside a core: they are what runs a system of cores, dispatching calls, evaluating guards, handing the token from one activation to the next. A definition of execution is not itself a program in the language it executes — exactly as [5]’s own account of a game meeting an adversary sits in their informal Section 3, outside the grammar of their Figure 15 — and the one notation that could be mistaken for a core’s own, the continuation form \(\id ''.\fopl {Op}(in'')\ \text {as}\ \id '''\,;\,k\) carrying an explicit, unbound resumption \(k\), belongs entirely to that outer layer: it never once occurs inside an operation’s own code from Chapter 13 on. A plainer relative of it does, constantly — an ordinary call to another functionality’s operation, resumed under the caller’s own identity rather than handed a fresh continuation — and that one is a core-language matter in its own right, below.
The core grammar. A core is a sequence of statements, and every operation this book writes is exactly one core. Scoped to what this book’s cores actually use, rather than to \(\mathcal {L}\)’s full grammar:
Figure 5: The core grammar, scoped to this book’s own usage. \(\mathcal {L}\)’s grammar ([5], their Figure 15) with the sub-grammar of expressions left to ordinary mathematical notation, since every expression this book writes is already standard over the six types below; \(\mathit {call}\) is \(\mathcal {L}\)’s own, generalized past their Adversary-only restriction (below). (Chapter 10.)
Six base types, not \(\mathcal {L}\)’s five: integer, boolean, string, set, table — \(\mathcal {L}\)’s array, kept as a function’s type throughout, \(\V {L} : \mathbb {N} \to \{0,1\}^{n} \cup \{\unset \}\) reading exactly as \(A : \{0,1\}^{*} \to \{0,1\}^{*} \cup \{\textsf {undefined}\}\) does there, \(\unset \) this book’s \(\textsf {undefined}\) — and identity, this book’s own addition, below. Only one \(\textbf {for}\)-form is attested, \(\textbf {for}\ x \in S\ \textbf {do}\), and the one instance of it binds a pair directly, \(\textbf {for}\ (m,y) \in N\ \textbf {do}\) (Chapter 20, lines 17 and 16) — an obvious sugar for binding one variable and destructuring it. The bounded integer-range form \(\mathcal {L}\) also allows is in reserve, unused so far, and licensed the moment a core needs it.
The caller is implicit. Every operation’s core is headed \(\id .\Op (in)\) from \(\id '\), and \(\id '\) — the caller’s identity — is readable anywhere in the core though it names no argument of \(\Op \). A plain oracle in \(\mathcal {L}\) carries nothing like it; this book’s cores need it because so many begin by asking exactly who is calling before anything else runs, \(\Gclock \)’s operations being representative (the guard at line 13 tests \(\id '.F\) and \(\id .P\)’s corruption before the core does anything else).
A core may call another core. \(\mathcal {L}\) reserves the \(\mathit {call}\) expression for the Adversary alone; an oracle inside one of their games may not place one. Every functionality, protocol and game in this book does — the protocol of Chapter 20 reads \(\Fpki \) and \(\Fsig \) mid-operation (lines 22 and neighbours), and \(\Frand \)’s own unpredictability game calls back into \(\Frand \) itself (line 5) — because this book’s functionalities and protocols are built from others by declaration, \(\uses \) naming exactly what a core may call (Chapter 1), and a game’s shell is a functionality like any other. The call itself is \(\mathcal {L}\)’s own, unrelaxed: \(\id ''.\Op (e_1,\ldots )\ \textbf {as}\ \id \) evaluates like any other expression and resumes the calling core at the same line, under its own identity. What stays strictly outside a core is the general form, with an unbound continuation \(k\) standing for an arbitrary resumption point rather than “the next line of this same core” — that is the execution model’s own notation for what a call means in general, never a core’s, and Section 3.6 is where it is defined.
Require is sugar. A core’s own \(\textbf {require}\ e\) line, used throughout the execution-model chapters and inside plenty of the cores to come, is sugar for \(\textbf {if not}\ e\ \textbf {then}\ \textbf {return}\ \none \) — not literally \(\rej \), even though a failed guard elsewhere returns exactly that. Section 3.6 makes \(\rej \) the one value no core may return as its own output, laundering a core-level \(\rej \) into \(\none \) before delivery; a core’s own \(\textbf {require}\) merely names the common case compactly. \(\Gclock \)’s operations spell the same guard out by hand, with an ordinary \(\textbf {if}\dots \textbf {then}\ \textbf {return}\) (line 13 again): both are the one core-language statement, sugared or not.
Table indices need no new rule. \(\V {reg}[\id .P]\), \(\V {L}[\V {ctr}]\): neither is string-indexed, and \(\mathcal {L}\) already has the answer, its own third enhancement ([5]) — a non-string index is passed through \(\mathrm {encode}(\cdot )\) first, silently. Every table this book writes that is not string-indexed already reads this way; there is nothing to add here beyond citing them for it.
Identity is a sixth type. One departure is not sugar. Definition 1.1 makes an identity a pair \(\id = (\PID ,P)\) of a process id and a party, a process id itself a triple \((F,s,i)\) — and a core reads through both levels at once, \(\id .F\), \(\id .s\), \(\id .P\) named projections, \(\id .i\) the one field no core ever reads (Chapter 1 says so outright). None of \(\mathcal {L}\)’s five types carries a projection, and \(\mathrm {encode}(\cdot )\) gives only equality-preservation, by [5]’s own account of it — an identity is read apart far too often for that to serve. So identity joins the type list as a sixth base type, structured rather than atomic, with projection and componentwise equality as its only operations — the one place this book’s cores ask \(\mathcal {L}\) for something it does not already have.
Reading the code. The grammar above is what a core may compute; how it is set on the page is a separate promise, and one already mostly kept. Keywords are bold, algorithmicx’s default: if, then, else, for, do, return, and require. An operation’s name carries a link wherever it is declared and wherever it is called back to, both rendered in accentsoft small caps — one macro anchors the declaration, two more point back to it from every call site. State lives in \(\V {x}\), typewriter, reserved for a core’s own mutable fields; \(\id \), \(in\), \(out\) stay italic, bound parameters rather than state, and the two must not be run together — a future reader deciding what a core’s own record type looks like needs exactly this distinction and no other. Comments print in commenttint, italic, off to the side, never load-bearing. That copy-editing pass over the chapters already written is done, not new notation but a uniformity sweep: a first prose mention of an already-declared operation is linked back to its declaration throughout, and the constant atoms — \(\ok \), \(\rej \), \(\true \), \(\false \), \(\done \), together with every trace tag and storage key elsewhere in this book — carry commenttint rather than an operation name’s own colour, so bare colour now does separate “this is a name” from “this is a value.”
What the grammar and the departures above buy, together, is a single test: from Chapter 13 on, a line of this book’s math is a core’s own code exactly when it type-checks against the table above plus the departures named here, and it is a specification — a game’s verdict, a property’s quantifier, \(\San \)’s own \(\mathrm {pick}\) — exactly when it does not. Closing the gap to an actual language, OCaml or otherwise, is then a matter of compiling six types and a handful of statement forms once, not of first deciding, chapter by chapter, what a given display of symbols was ever claiming to compute.