Definition 4.11 is stated against arbitrary classes and says nothing about what they contain. Filling them with machines of bounded resources turns each statement of the previous section into a concrete one, and the relations between classes into arithmetic on budgets.
Definition 4.30 (Budgets and bounded classes). A budget is a pair \(\bd {a} = (t,r)\) of naturals. A machine is \(\bd {a}\)-bounded if it takes at most \(t\) steps in each invocation and answers at most \(r\) calls in all; so it runs for at most \(t\,r\) steps in any execution. A machine meeting both bounds in every execution is counted \(\bd {a}\)-bounded whether or not the halting rule is written into it — the bundles built from bounded machines below are bounded in this sense. Write \(\Aset (\bd {a})\), \(\SimSet (\bd {a})\) and \(\ZenvSet _{\pi ,\varphi }(\bd {a})\) for the classes of \(\bd {a}\)-bounded adversaries, of \(\bd {a}\)-bounded simulators, and of \(\bd {a}\)-bounded environments lying in \(\ZenvSet _{\pi ,\varphi }\). Budgets are ordered componentwise; machines that share an execution — a bundle of several, or a simulator running an adversary — combine by
one machine running per activation, so the per-invocation time takes the larger bound while the invocation counts add.
The budget is part of the machine, not a promise about it. Bounding the three slot machines is not yet enough to bound an execution — the members of a system are machines too, and a core that recurses on itself, or two members calling one another forever, would carry the token away from every budgeted machine with nothing to reclaim it. Concrete statements therefore read over budgeted systems: every member of every system compared carries a budget of its own, in the sense of this definition applied verbatim. An execution then runs finitely many machines, each taking finitely many steps, and exactly one machine steps at any moment, so the execution halts within the total step bound \(\sum _i t_i\,r_i\) of its machines and \(\opl {Exec}\) is defined outright. Halting at a budget is given a value: a machine that halts mid-call resumes each caller suspended on it with \(\none \), and an environment that halts away from its root return is read as returning \(0\). The classes are monotone in the budget, \(\Aset (\bd {a}) \subseteq \Aset (\bd {a}')\) whenever \(\bd {a} \leq \bd {a}'\), and likewise for \(\SimSet \) and \(\ZenvSet _{\pi ,\varphi }\). That makes Lemma 4.23 a statement about numbers: shrinking the adversary budget, growing the simulator budget, or shrinking the environment budget each preserve emulation.
Definition 4.31 (Concrete UC advantage). Let \(\pi \) and \(\varphi \) be budgeted systems, let \(\bd {a}\) and \(\bd {s}\) be budgets for the adversary and the simulator, and let \(\ZenvSet \subseteq \ZenvSet _{\pi ,\varphi }\) be a class of environments. Set
and abbreviate \(\advtg ^{\op {uc}}_{\pi ,\varphi }[\bd {a},\bd {s},\bd {z}]\) for the case \(\ZenvSet = \ZenvSet _{\pi ,\varphi }(\bd {z})\), the largest class of that budget.
The third argument is a class rather than a budget because the largest class depends on the pair of systems, and the statements below compare advantages taken over different pairs. Where a common class is needed the notation must be able to say so.
The three operators are the three quantifiers of Definition 4.11 read as a value, in the same order and for the same reason: the simulator is chosen after the adversary and before the environment. The extrema are attained, though the reason takes a moment, and it is finiteness rather than compactness. An \(\bd {a}\)-bounded machine takes at most \(t\,r\) steps in all, so it reads at most \(t\,r\) symbols of any input and at most \(t\,r\) coins; up to behaviour it is a map from what it read to what it did, and there are finitely many such maps. Its coins weight them with dyadic probabilities of denominator \(2^{t r}\), so a bounded class induces finitely many behaviour distributions in all. With the members of the systems budgeted as well, \(\Pr [\opl {Exec} = 1]\) is a well-defined number at each choice of behaviours, so each advantage of Definition 4.5 takes one of finitely many values, and a maximum or minimum over finitely many values is attained. (Over an arbitrary class \(\ZenvSet \) the outer \(\max \) is read as a supremum.) Therefore
holds exactly when that quantity is at most \(\varepsilon \) — the attained minimum is what makes the reverse direction exact at the boundary. A concrete security claim is then a single inequality relating three budgets and a probability, with no security parameter and no asymptotics in sight.