README.md

Games

This folder holds games: random systems whose replies carry a bit, the MBO, which once set stays set. It defines the visible system, winning, conditional equivalence and equivalence as games; proves that distinguishing is bounded by winning, the fundamental lemma and the until-bad bound for games; lifts converters to games; and presents games by discrete games and by sampled functions with a hidden condition. The random systems, distinguishers and distances it uses are those of RandomSystems and Distance. Citations refer to the numbered references of THEORY.md.

Games, winning and conditional equivalence

A game is a random system whose replies carry a bit, the MBO, which once set stays set [3, §3.7.1]. Its visible system $G^-$ ignores the MBO [3, Definition 4.18]: the probability of a transcript, whatever the MBOs. A distinguisher used as a winner does not see the MBO, and its winning probability is the probability that the MBO is set when it stops [3, Definition 4.5]. A game is conditionally equivalent to a random system $T$, $G \mathrel{|\!\equiv} T$, when it replies as $T$ as long as the MBO is unset [3, Definition 4.19], [5, Definition 13]. The advantage between the visible system and $T$ is then at most the winning probability [3, Lemma 4.16 and the proof of Theorem 4.17]:

$$G\big(x^n, (y, 0)^n\big) = \Pr_G[\text{MBO unset} \mid x^n]\ T(x^n, y^n) \quad \Longrightarrow \quad \mathrm{Adv}_P(G^-, T) \le \Pr[P \text{ wins } G] .$$

Before the MBO is set, the winner sees the replies of $T$, which carry no information about the MBO. If the MBO is set with probability at most $\varepsilon$ on every fixed query sequence, every winner wins with probability at most $\varepsilon$. The transcript distance is the largest advantage (Distance), so the visible system is then within $\varepsilon$ of $T$ [3, Theorem 4.17], [5, Theorem 3], for $G$ and $T$ replying at the queried label:

$$G \mathrel{|\!\equiv} T, \quad \Pr_G[\text{MBO set} \mid x^n] \le \varepsilon \ \text{ for every fixed } x^n \quad \Longrightarrow \quad \Delta(G^-, T) \le \varepsilon .$$

Equivalence as games

Two games are equivalent as games, $G \overset{g}{\equiv} H$, when they behave alike as long as the MBO is unset: they give every transcript with every MBO unset the same probability [3, Definition 4.16], [4, Definition 5]. A distinguisher then wins both alike [3, Lemma 4.15], and by the fundamental lemma its advantage between their visible systems is at most its winning probability [3, Lemma 4.16], [4, Lemma 7 and Theorem 1 (i)]: to tell them apart, it must set the MBO. For games replying at the queried label:

$$G\big(x^n, (y, 0)^n\big) = H\big(x^n, (y, 0)^n\big) \quad \Longrightarrow \quad \mathrm{Adv}_P(G^-, H^-) \le \Pr[P \text{ wins } G] = \Pr[P \text{ wins } H] .$$

Identical until bad

For games, identical until bad rests on the systems-level bound of Distance: two random systems whose transcript probabilities lie above a common part are within $\varepsilon$ of each other when each step loses little of it. On a game $G$, the part with every MBO unset lies below the visible system, and a step loses from it the probability that $G$ sets the MBO at that step. Suppose that, from every transcript with every MBO unset, $G$ sets the MBO at the next query $x$ with probability at most $\beta(h, x)$ times the probability of the transcript. The mass missing from the unset part along the transcripts of a winner is the winning probability, so every winner wins with probability at most $\varepsilon$. Two games equivalent as games have the same unset part, which is therefore a common part of their visible systems, and the per-step costs bound its missing mass: the visible systems are within $\varepsilon$ of each other. Two discrete games are equivalent as games when they are coupled: a joint law of the two [1, Theorem 2] whose pairs have one condition and systems that answer alike while the condition does not hold.

Attachment

The library defines the action of a PDC $\alpha$ on a game by its MBO-forwarding lift $\hat\alpha$: the lift runs $\alpha$, which does not see the inside MBOs, and gives each outside reply the MBO of the latest inside reply. The source states this action informally: a converter turns a game into a game, the MBO being neither seen nor affected by the converter [3, §4.7.2]. The lift is functorial: it preserves identities, $\hat{\mathrm{id}} = \mathrm{id}$, and composition, $\widehat{\alpha \beta} = \hat\alpha \hat\beta$. It keeps games games and commutes with the visible system, $(\hat\alpha G)^- = \alpha\, G^-$. A winner with $\alpha$ absorbed wins $G$ as the winner wins $\hat\alpha G$ [3, §4.7.2, equation (4.9)]. A solver behavior pairs a probabilistic distinguisher's probability of outputting 1 on each random system with its winning probability for each game, and absorbing a PDC into a solver behavior gives a solver behavior.

Discrete games

Discrete games present games, as PDSs present random systems. A discrete game is a distribution over deterministic discrete games, pairs of a DDS and a hidden monotone condition on the queries, on a domain [2, Definitions 2.20–2.22]. Each reply of a deterministic discrete game carries the condition on the queries so far as its MBO, and a discrete game presents the game of these systems. Its visible system is the behavior of the visible systems, and on an admitted query sequence the MBO is unset with the probability that the condition does not hold, so a bound on the condition at the empty and every admitted query sequence bounds the probability that the MBO is set. The game is conditionally equivalent to a random system $S$ when the replies with the condition unset factor through $S$:

$$\Pr_G[\,y^n,\ \lnot\mathrm{bad} \mid x^n\,] = \big(1 - \Pr_G[\mathrm{bad} \mid x^n]\big)\, S(x^n, y^n) .$$

A sampled function with a hidden condition is a discrete game, and the game it presents is conditionally equivalent to the ideal function once, on every fixed query sequence, the answers jointly with the unset condition factor through the ideal answers.