In an execution exactly one machine holds the activation token. A call \(out \gets \id .\Op (in)\) abbreviates suspending the caller with a continuation and passing the token to interface \(\Op \) of \(\F \) at identity \(\id \). Every call between machines addresses a full interface, and \(\fopl {Op}\) is what \(\opl {Exec}\) dispatches; a core is invoked only by the wrapper that serves it, inside the machine that carries it, and never across a token transfer. A call addressed to an identity no machine occupies is answered with \(\rej \). An instance may hold several outstanding continuations and may be re-entered while suspended, in particular by \(\Adv \).
Definition 3.3 (Machines and occupancy). A machine is anything an execution runs: the members of the system, and whatever the execution supplies alongside them. A machine occupies a finite set of identities — for a functionality, the \(\IDs (\F )\) of Definition 1.1 — and \(\opl {Exec}\) dispatches to it exactly the calls addressed to identities it occupies. The occupants of one execution carry pairwise disjoint identity sets, and \(\opl {Exec}\) is defined for no other family. An occupant of the adversary slot is a machine occupying the identities of process id \(A\) and no others; the adversary of Section 3.4 is one, and so is every simulator of Chapter 4. An activation is a maximal interval during which one machine holds the token.
Every call carries a claimed id \(\id '\). Standard functionalities may claim only the identity of the interface placing the call; \(\Zenv \) and \(\Adv \) may claim others, subject to the checks of Chapter 2. Those checks are the guard, which tests \(\id '\) against the interface’s identity \(\id \) and against the functionality’s parameters, and we specify them with require statements. A failed guard returns the distinguished value \(\rej \) to the sender, and \(\rej \) is a refusal rather than a value: no machine may return it as its own output. The rule is enforced rather than assumed — a core whose code would return \(\rej \), and a mediated answer of \(\rej \) from the adversary’s slot, are delivered as \(\none \) instead — so a caller receiving \(\rej \) learns that a guard refused its call, and nothing else can produce one. In particular \(\rej \neq \none \).
Randomness is per machine: each machine carries its own coin tape, infinite, uniform, and independent of every other machine’s, read only when its code samples. Probabilities over an execution are over these tapes jointly. Bundling machines into one occupant — as Chapter 4 and Section 4.4 do — does not merge tapes: a hosted copy’s coins are what they were before absorption.
Besides the system \(\pi \), the execution carries three machines: the environment \(\Zenv \), the adversary \(\Adv \), and the corruption register \(\Corr \), whose state \(\Cs \) every wrapper reads. By Chapter 1 none is a member of \(\pi \), which makes line 1 unambiguous — the register is initialized once, as an argument, not a second time as a member — and keeps \(\pi \) the object a designer wrote. The procedure initializes the three, then activates the environment at \((Z,Z)\) as though it had called itself. That first activation goes through \(\Zenv \)’s full interface like any other, so the environment is silenced from the outset, and \(\opl {Guard}_{\Zenv }\) passes trivially, the claimed and target identities being the same. Whatever the environment returns is the outcome.
Execution \(\opdef {Exec}\)
system \(\pi \), environment \(\Zenv \), adversary \(\Adv \), corruption register
\(\Corr \)
\(\opl {Exec}(\pi ,\Zenv ,\Adv ,\Corr )\):
Read as a handler [12, 4], the execution has exactly one operation: placing a call. Line 2 activates the environment, the only activation not placed by a machine. Line 4 handles every call thereafter, and the continuation \(k\) is where the token comes back: suspending the caller, passing the token to \(\id \), and resuming the caller with the answer are precisely what invoking \(k\) on that answer means. Exactly one machine holds the token throughout. The return clause is reached when the environment’s program halts, and its output is the execution’s.