From 60fe46d373c1788f2bdfaae74f824eb94873c51c Mon Sep 17 00:00:00 2001 From: Marc Ilunga Date: Tue, 13 Oct 2026 20:12:01 +0100 Subject: [PATCH 1/2] Docs: THEORY.md shows the structure, details in module READMEs THEORY.md keeps the layers, the central objects, the class-to-instance table and the departures, and the rest moves to READMEs next to the code (Probability, RandomSystems with Distance, Game and Typed, ConstructiveCryptography, Examples) and to the DSL's GRAMMAR.md. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9 --- README.md | 21 +- THEORY.md | 1450 +++---------------- src/ConstructiveCryptography/DSL/GRAMMAR.md | 141 +- src/ConstructiveCryptography/README.md | 416 ++++++ src/Examples/README.md | 141 ++ src/Probability/README.md | 80 + src/RandomSystems/Distance/README.md | 162 +++ src/RandomSystems/Game/README.md | 154 ++ src/RandomSystems/README.md | 207 +++ src/RandomSystems/Typed/README.md | 158 ++ 10 files changed, 1669 insertions(+), 1261 deletions(-) create mode 100644 src/ConstructiveCryptography/README.md create mode 100644 src/Examples/README.md create mode 100644 src/Probability/README.md create mode 100644 src/RandomSystems/Distance/README.md create mode 100644 src/RandomSystems/Game/README.md create mode 100644 src/RandomSystems/README.md create mode 100644 src/RandomSystems/Typed/README.md diff --git a/README.md b/README.md index 4ae165c..0e21ff0 100644 --- a/README.md +++ b/README.md @@ -12,20 +12,21 @@ composable security is given in [7]. ## Libraries The sources are under `src/`; module names follow their paths there. [THEORY.md](THEORY.md) -summarizes the theory layer by layer, with links to the Lean declarations. +shows the layers and how they connect, with each class and its instance. The READMEs linked in +the table give the details of each library, with links to the Lean declarations. | Library | Content | |---|---| -| `Probability` | finitely supported distributions, kernels, statistical distance, couplings, expectation, counting | -| `RandomSystems` | systems and automata; deterministic converters and programs; distributions over deterministic systems; random systems given by their cumulative probabilities; probabilistic automata and memoryless systems; probabilistic converters, attachment and parallel composition; transcript distance and distinguishers; games; typed systems, typed converters and typed games on interfaces, with filters, contexts, sources, automata, memoryless and functional systems, and games presented by discrete games; the programs and program converters of the DSL | -| `ConstructiveCryptography.Specification`, `.Construction` | specifications, constructions and relaxations over any carrier | -| `ConstructiveCryptography.CryptographicAlgebra` | the classes of cryptographic algebras: resource theories, parallel composition, compatible pseudo-metrics and distinguisher classes, relaxations | -| `ConstructiveCryptography` (top level) | the instances of the classes on interfaces (category, monoidal category, cryptographic algebra, distinguisher class, games), each field a systems-level object; notation | -| `ConstructiveCryptography.Substitution` | the substitution calculus for constructions [6] | -| `ConstructiveCryptography.DSL` | a compiler from component declarations to typed systems and typed converters | -| `ConstructiveCryptography.Tactics` | proof commands, including the substitution calculations `cc_calc` | +| [`Probability`](src/Probability/README.md) | finitely supported distributions, kernels, statistical distance, couplings, expectation, counting | +| [`RandomSystems`](src/RandomSystems/README.md) | systems and automata; deterministic converters and programs; distributions over deterministic systems; random systems given by their cumulative probabilities; probabilistic automata and memoryless systems; probabilistic converters, attachment and parallel composition; transcript distance and distinguishers ([`Distance`](src/RandomSystems/Distance/README.md)); games ([`Game`](src/RandomSystems/Game/README.md)); typed systems, typed converters and typed games on interfaces, with filters, contexts, sources, automata, memoryless and functional systems, and games presented by discrete games ([`Typed`](src/RandomSystems/Typed/README.md)); the programs and program converters of the DSL | +| [`ConstructiveCryptography.Specification`, `.Construction`](src/ConstructiveCryptography/README.md#specifications-and-constructions) | specifications, constructions and relaxations over any carrier | +| [`ConstructiveCryptography.CryptographicAlgebra`](src/ConstructiveCryptography/README.md#the-classes) | the classes of cryptographic algebras: resource theories, parallel composition, compatible pseudo-metrics and distinguisher classes, relaxations | +| [`ConstructiveCryptography`](src/ConstructiveCryptography/README.md#the-instances-on-interfaces) (top level) | the instances of the classes on interfaces (category, monoidal category, cryptographic algebra, distinguisher class, games), each field a systems-level object; notation | +| [`ConstructiveCryptography.Substitution`](src/ConstructiveCryptography/README.md#the-substitution-calculus) | the substitution calculus for constructions [6] | +| [`ConstructiveCryptography.DSL`](src/ConstructiveCryptography/DSL/GRAMMAR.md) | a compiler from component declarations to typed systems and typed converters | +| [`ConstructiveCryptography.Tactics`](src/ConstructiveCryptography/DSL/GRAMMAR.md#proof-commands) | proof commands, including the substitution calculations `cc_calc` | | `Commons` | common ideal systems (URF, URP and their strong and tweakable forms, memoryless sources), the CDH assumption as a pair of systems, the security notions as pairs of systems [6]: symmetric encryption (real-or-random and left-or-right CPA) and authenticated encryption (ind-cca, int-ptxt, int-ctxt, ae), public-key encryption and KEMs (IND-CPA, IND-CCA), MACs and signatures (EUF-CMA, SUF-CMA), PRGs, universal hashing (UHF, DUF) and collision resistance, and the schemes SHA-256, SHA-3, SHAKE, Keccak-256, ML-KEM [9] and ML-DSA [10] (the last two adapted from VCVio [11]) with known-answer tests, in the order of [8] | -| `Examples` | authenticated encryption, AES, AEAD, PRG length extension, substitutions on interfaces, the proof commands | +| [`Examples`](src/Examples/README.md) | authenticated encryption, AES, AEAD, PRG length extension, substitutions on interfaces, the proof commands | | `Tests` | axiom audits, counterexamples, DSL diagnostics and semantics, tests of the substitution calculus | Module docstrings cite the source of each definition and theorem, with the diff --git a/THEORY.md b/THEORY.md index f827246..9e1e6cc 100644 --- a/THEORY.md +++ b/THEORY.md @@ -1,20 +1,23 @@ # The theory, layer by layer -This is a cheat-sheet of what the library formalizes. It starts at the systems level: **random -systems** and their properties, and **typed systems**, the random systems and converters on the -alphabets and domain of an interface. Then come the **abstract layers** (classes of assumptions, -up to categories), each shown with the instance that connects it to the systems: every field of -the instance is a systems-level object and every axiom a systems-level theorem. It ends with what -the layers are used for: **constructions**, the **substitution calculus**, the **DSL** and the -**examples**. Every notion and result is linked, in the text, to its Lean declaration; citations -refer to the [references](#references) at the end. +This page shows the structure of the library: its layers, the central objects of each, and how +they connect. The systems level holds the concrete objects: **random systems**, and **typed +systems**, the random systems and converters on the alphabets and domain of an interface. The +abstract layers are **classes of assumptions**, up to categories. **Instances** connect the two: +every field of an instance is a systems-level object, and every axiom is discharged by a +systems-level theorem. The layers are used for **constructions**, the **substitution calculus**, +the **DSL** and the **examples**. Each section links its central declarations and points to the +README of its folder for the rest; citations refer to the [references](#references) at the end. ``` -Probability ─▶ Random systems, typed systems ══ instance ══▶ Classes - (App. A) (§1, §2) (§3) - ▲ │ - DSL (§6) ▼ - Constructions (§4) ─▶ Substitution (§5) +Probability ─▶ Random systems ─▶ Typed systems ══ instance ══▶ Classes + (§1) (§2) (§3) + ▲ │ + │ ▼ + DSL (§5) Constructions, substitution (§4) + │ + ▼ + Examples (§5) ``` --- @@ -23,26 +26,14 @@ Probability ─▶ Random systems, typed systems ══ instance ══▶ Class *Systems over finite alphabets, answering exactly on a bounded domain [1], [2, Chapter 2], [3, Chapter 3]. Laws are finitely supported distributions and $`\delta`$ is the statistical -distance (Appendix A).* +distance ([Probability](src/Probability/README.md)).* -### 1.1 Deterministic systems - -A [**deterministic system**][IsDDS] (DDS) is a [partial function][System] from input histories to -the next output, $`s : \mathcal X^{*} \rightharpoonup \mathcal Y`$, [silent at the empty -history][SilentAtEmpty], whose domain is [closed under nonempty prefixes][PrefixClosed]. Systems -are [wired together][interconnect], each output leaving the wiring or returning as an input. A -system [replies][Replies] $`y_1 \dots y_n`$ to $`x_1 \dots x_n`$ when it answers each prefix with the -next output, and a DDS [is determined by its completed replies][IsDDS.eq_of_replies_iff]. An -[automaton][automatonSystem] is a transition function started in a state, and -[bisimilar][IsBisim] automata [have the same system][automatonSystem_eq_of_bisim]. An -[environment][DDE] (DDE) chooses the next query from the replies so far. - -### 1.2 Probabilistic systems - -A [**domain**][Domain] $`\mathcal D`$ admits next queries after each transcript, with a bound on the -length. A [**PDS**][PDS] is a finite distribution over DDSs [with domain][HasDomain] -$`\mathcal D`$ [1, Definition 8]. A [**random system**][RandomSystem] is given by its cumulative -probabilities $`p`$ on transcripts [1, after Lemma 5], [normalized][IsRandomSystem] on the domain: +**Systems.** A [deterministic system][IsDDS] (DDS) is a partial function from input histories to +the next output, whose domain is closed under nonempty prefixes. A [domain][Domain] +$`\mathcal D`$ admits next queries after each transcript, with a bound on the length, and a +[PDS][PDS] is a finite distribution over DDSs with domain $`\mathcal D`$ [1, Definition 8]. A +[**random system**][RandomSystem] is given by its cumulative probabilities $`p`$ on transcripts +[1, after Lemma 5], [normalized][IsRandomSystem] on the domain: ```math p(\varepsilon) = 1, \qquad p \ge 0, \qquad @@ -50,385 +41,91 @@ p(\varepsilon) = 1, \qquad p \ge 0, \qquad \begin{cases} p(h) & \text{if } x \text{ is admitted after } h, \\ 0 & \text{otherwise.} \end{cases} ``` -A PDS [has a random system][PDS.behavior], and [equivalent][Equivalent] PDSs -[have the same one][PDS.behavior_eq_iff]. Every random system -[has a finite presentation][RandomSystem.exists_presentation], so random systems -[are exactly the classes of equivalent PDSs][RandomSystem.ofPDSClass_bijective]. Two random -systems [are equal exactly when][RandomSystem.eq_iff_sLaw] their -[transcript laws][RandomSystem.sLaw] agree in every [compatible][RandomSystem.Compatible] -environment, and on a domain of input histories -[fixed query sequences suffice][RandomSystem.eq_iff_sLaw_fixedQueries] [1, Lemma 5]. Random -systems on one domain form [mixtures][RandomSystem.mix], and two random systems run -[independently in parallel][RandomSystem.parallel] form one on the combined alphabets. - -A [**probabilistic automaton**][RandomSystem.ofProbAutomaton] answers a query from its state with a -law on the next state and the reply, a [probabilistic step][ProbStep]; its random system follows -the [sub-law of the states][ProbStep.belief] reached with the replies of a transcript, whose weight -is the probability of the transcript. On an input domain, two probabilistic automata -[have the same random system][RandomSystem.ofProbAutomaton_eq_of_simulation] along a -[simulation][ProbStep.SimulatesAt], a kernel between their states through which their steps -commute. A deterministic automaton with a random initial state -[is the probabilistic automaton of its point steps][RandomSystem.ofProbAutomaton_ofDeterministic_apply], -and a probabilistic automaton -[is a deterministic automaton reading pre-sampled draws][RandomSystem.ofProbAutomaton_eq_drawStep], -sampled once with the initial state: a random automaton [4, Definition 2]. - -A random system is [**memoryless**][RandomSystem.memoryless] when the law of its reply depends only -on the current query, never on the history: a source "can be memoryless or have memory" -[3, Definition 3.1], and a single-input system given by a conditional distribution is a "discrete -memoryless channel" [3, §3.6.1]. With the reply law $`\nu`$, its probabilities obey the chain rule - -```math -p\big(h \cdot (x, y)\big) = p(h)\, \nu_x(y) \qquad \text{for every query } x \text{ admitted after } h, -``` - -and [a random system obeying it is the memoryless system][RandomSystem.eq_memoryless_of_snoc]. -A probabilistic automaton whose step [replies from every state with the same -law][ProbStep.Memoryless] $`\nu`$ [is the memoryless system of this law][RandomSystem.ofProbAutomaton_eq_memoryless]. -Two memoryless systems [side by side are memoryless][RandomSystem.parallel_memoryless]: a query -to either system is answered with the reply law of that system. - -### 1.3 Converters - -A [**DDC**][IsDDC] is a system on the converter alphabets (outside queries and inside replies in; -inside queries and outside replies out) with at most $`b`$ consecutive inside queries -[3, Definition 3.8]. A **DDC from $`E`$ to $`F`$** ([`IsDDCFrom`][IsDDCFrom]) answers exactly the -[converter domain][converterDomain] and queries only in $`E`$; attached to a system with domain $`E`$ -it [gives one with domain][IsDDCFrom.mapsDomain] $`F`$. A [**PDC**][PDCBehavior.ofPDC] is a distribution over DDCs, and -its [**behavior**][PDCBehavior] is a random system over the converter domain -[3, Definitions 3.17–3.18]. - -[Serial composition][serialM] $`\beta \odot \alpha`$ connects the inside of $`\beta`$ to the outside -of $`\alpha`$, and [DDCs compose][IsDDC.comp] with the product of their bounds. PDC behaviors have a -[composition][PDCBehavior.comp] and an [identity][PDCBehavior.id], with -[associativity][PDCBehavior.comp_assoc] and the [left][PDCBehavior.id_comp] and -[right][PDCBehavior.comp_id] identity laws. [Attachment][PDCBehavior.attach] samples the PDC, then -attaches the sample deterministically: [presentations attach to -presentations][PDCBehavior.attach_presents], [the identity leaves a system -unchanged][PDCBehavior.attach_id], and [a composition attaches its inner converter -first][PDCBehavior.attach_comp]. [Parallel composition][PDCBehavior.tensor] samples two PDCs -independently and runs them side by side, with [interchange][PDCBehavior.comp_tensor] against -serial composition. - -A [**program**][Program] is a deterministic oracle body: from its state, the outside query and the -inside exchanges of the current invocation, it computes the reply or the next inside query. A -program can be [bounded][Program.Bounded] (at most $`b`$ inside queries per invocation), have -[exact costs][Program.Costs], or [preserve a partial port map][Program.PortPreserving] -$`\iota : O \to \mathrm{Option}\ J`$: an invocation at $`o`$ queries the labels in the image of -$`\iota`$ only at $`\iota(o)`$, at most once, and none of them when $`\iota(o)`$ is none, so it -queries $`\iota(o)`$ [at most as often as it is queried at][DDC.insideQueries_restrict_length_le] -$`o`$. On an outside domain, a bounded program -[is a DDC from every inside domain containing its inside queries][DDC.ofProgramOn_isDDCFrom]. -Attached to an automaton, a program is [inlined][Program.inline] [4, §3.3]: the result is the -[combined automaton][Program.combine] on pairs of states, also -[on domains][Program.trim_apply_ofProgramOn_automaton]. - -Run against a probabilistic automaton, a program is the probabilistic automaton -[on pairs of states][Program.probCombine] whose step runs one invocation, the automaton answering -the inside queries with fresh steps; it [respects simulations][RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation]. -[**Attaching the program's converter to a probabilistic automaton is the program run against -it**][PDCBehavior.attach_ofDDC_ofProgramOn_ofProbAutomaton], the combined system $`C(F)`$ of a -system $`C(\cdot)`$ invoking $`F`$ [4, §3.3]; for point steps it is the -[combined automaton][PDCBehavior.attach_ofDDC_ofProgramOn_ofDeterministic]. Against memoryless -replies of the laws $`\nu`$, a program [replies memorylessly][Program.memoryless_probCombine] when -its [reply law][Program.replyLaw] $`\kappa`$, the law of one invocation whose inside queries are -answered by fresh samples of $`\nu`$, is the same from every program state. So [the composition law][PDCBehavior.attach_ofDDC_ofProgramOn_memoryless] -holds, whatever the number of the program's inside queries: - -```math -\alpha_P\, \mathrm{mem}(\nu) = \mathrm{mem}(\kappa). -``` - -### 1.4 Distance and distinguishers - -The [**transcript distance**][RandomSystem.transcriptDistance] takes the supremum over environments -$`E`$ [compatible with the domain][Domain.Compatible] and [bounded][QueryBounded] to $`n`$ queries; a -[**probabilistic distinguisher**][Domain.Distinguisher] $`P`$ [1, Definition 9] has an -[advantage][Domain.Distinguisher.advantage]: - -```math -\Delta(R, S) = \sup_{E,\, n}\ \delta\big(\mathrm{tr}(R, E, n),\ \mathrm{tr}(S, E, n)\big), -\qquad -\mathrm{Adv}_P(R, S) = \big\lvert \Pr[P(R) = 1] - \Pr[P(S) = 1] \big\rvert . -``` - -A probabilistic distinguisher is a distribution over -[deterministic distinguishers][IsDDD] [compatible with the domain][Domain.DecisionCompatible], and its -[probability of outputting 1][Domain.Distinguisher.probability] averages their -[decision probabilities][RandomSystem.decisionProbability]. For each $`P`$, $`\mathrm{Adv}_P`$ is a -pseudo-distance: it is [zero on equal systems][advantage_self], [symmetric][advantage_symm], and -[satisfies the triangle inequality][advantage_triangle]. The transcript distance -[is the largest advantage][RandomSystem.transcriptDistance_eq_iSup], -$`\Delta(R, S) = \sup_P \mathrm{Adv}_P(R, S)`$, so -[every advantage is at most the distance][advantage_le_transcriptDistance]. - -The [**behavior**][Domain.DistinguisherBehavior] of a probabilistic distinguisher is its -probability of outputting 1 on each system, as the behavior of a PDC is its random system; the -transcript distance [is also the largest advantage of a behavior][RandomSystem.transcriptDistance_eq_iSup_behavior]. - -**Couplings**: the [transcript][System.tr] $`\mathrm{tr}(s, E, n)`$ of a deterministic system $`s`$ -with an environment $`E`$ within $`n`$ rounds is the sequence of their query–reply pairs -[1, Definition 7]. For an environment compatible with the random system $`R`$ of a PDS $`P`$, the -transcript law of $`R`$ [is the transformation][PDS.sLaw_behavior_eq_fTransform] of $`P`$ by -$`\mathrm{tr}(\cdot, E, n)`$ [1, Definition 4 and footnote 9]. A [coupling][IsCoupling] $`J`$ of -$`P`$ and a PDS $`Q`$ with random system $`S`$ therefore bounds the distance of the transcript laws -by the [probability that the transcripts differ][PDS.statDist_sLaw_behavior_le_of_isCoupling], and -the transcript distance by the -[probability that the systems differ][PDS.transcriptDistance_behavior_le_of_isCoupling]: - -```math -\delta\big(\mathrm{tr}(R, E, n),\ \mathrm{tr}(S, E, n)\big) -\le \Pr_{(s, t) \sim J}\big[\mathrm{tr}(s, E, n) \ne \mathrm{tr}(t, E, n)\big], -\qquad -\Delta(R, S) \le \Pr_{(s, t) \sim J}[s \ne t] . -``` - -The second bound holds for every coupling; [1, Theorem 2] states in addition that some -presentations of $`R`$ and $`S`$ have a coupling attaining it. - -**Absorption**: [absorbing][DistinguisherBehavior.absorb] a PDC $`\alpha`$ into a behavior $`d`$ gives -$`d \circ \alpha`$, which decides on a system as $`d`$ decides on $`\alpha`$ attached to it, -$`\Pr[(d \circ \alpha)(R) = 1] = \Pr[d(\alpha R) = 1]`$. Absorbing a serial composition -[absorbs its PDCs in turn][DistinguisherBehavior.absorb_comp], -$`d \circ (\beta \circ \alpha) = (d \circ \beta) \circ \alpha`$. On deterministic distinguishers -absorption [connects the distinguisher to the converter's outside][absorbAll]; absorbing a -converter into a probabilistic distinguisher [gives a probabilistic distinguisher][Domain.Distinguisher.exists_absorbAll], -so $`d \circ \alpha`$ is a behavior, and so does absorbing -[a system run beside][Domain.Distinguisher.exists_absorbRight]. - -**Restriction**: the [restriction][RandomSystem.restrict] $`R \restriction D'`$ of a random system on $`D`$ -to a smaller domain $`D' \subseteq D`$ keeps the masses of the transcripts $`D'`$ admits and is zero -elsewhere. Restrictions [compose][RandomSystem.restrict_restrict], and an environment compatible -with $`D'`$ [sees the transcript law of the system itself][RandomSystem.sLaw_restrict], so restriction -[does not increase the distance][RandomSystem.transcriptDistance_restrict_le], -$`\Delta(R \restriction D', S \restriction D') \le \Delta(R, S)`$. - -**H-coefficient bound**: under an environment $`E`$, the transcript law of $`R`$ gives each -transcript $`h`$ that $`E`$ produces the probability $`R(h)`$, and the others zero; the restriction -is the same for $`S`$, so a ratio of the two systems' probabilities on the good transcripts is a -ratio of their transcript laws. For $`R`$ and $`S`$ replying at the queried label, Patarin's -H-coefficient technique then -[bounds the distance][RandomSystem.transcriptDistance_le_add_of_ratio_on_good] by the error -$`\varepsilon_1`$ of the ratio and the bound $`\varepsilon_2`$ on the bad transcripts under $`S`$: - -```math -(1 - \varepsilon_1)\, S(h) \le R(h) \ \text{ for } h \notin \mathrm{Bad}, \quad -\Pr_{\mathrm{tr}(S, E, n)}[\mathrm{Bad}] \le \varepsilon_2 \ \text{ for all } E, n -\quad \Longrightarrow \quad -\Delta(R, S) \le \varepsilon_1 + \varepsilon_2 . -``` - -### 1.5 Games - -A [**game**][RandomSystem.MonotoneMBO] is a random system whose replies carry a bit, the MBO, -which once set stays set [3, §3.7.1]. Its [**visible system**][RandomSystem.visible] $`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][DDE.blindMBO], and its -[**winning probability**][RandomSystem.winProbability] is the probability that the MBO is set when -it stops [3, Definition 4.5]. A game is [**conditionally equivalent**][RandomSystem.ConditionallyEquivalent] -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][Domain.Distinguisher.advantage_le_winProbability] -[3, Lemma 4.16 and the proof of Theorem 4.17]: - -```math -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][Domain.Distinguisher.winProbability_le_of_unsetProbability] $`\varepsilon`$. -The transcript distance is the largest advantage (§1.4), so the visible system is then -[within][RandomSystem.transcriptDistance_visible_le_of_unsetProbability] $`\varepsilon`$ of $`T`$ -[3, Theorem 4.17], [5, Theorem 3], for $`G`$ and $`T`$ replying at the queried label: - -```math -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 . -``` - -Two games are [**equivalent as games**][RandomSystem.GameEquivalent], $`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][Domain.Distinguisher.winProbability_eq_of_gameEquivalent] [3, Lemma 4.15], and -by the fundamental lemma its advantage between their visible systems is -[at most its winning probability][Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent] -[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: +A PDS [has a random system][PDS.behavior], and every random system +[has a finite presentation][RandomSystem.exists_presentation]: random systems +[are exactly the classes of equivalent PDSs][RandomSystem.ofPDSClass_bijective]. + +**Converters and attachment.** A [DDC][IsDDC] is a system on the converter alphabets with a bound +on its consecutive inside queries [3, Definition 3.8]. A [PDC][PDCBehavior.ofPDC] is a distribution +over DDCs, and its [behavior][PDCBehavior] is a random system over the converter domain +[3, Definitions 3.17–3.18]. PDC behaviors [compose][PDCBehavior.comp] associatively, with an +[identity][PDCBehavior.id]. [Attachment][PDCBehavior.attach] $`\alpha R`$ samples the PDC, then +attaches the sample: [the identity leaves a system unchanged][PDCBehavior.attach_id], and +[a composition attaches its inner converter first][PDCBehavior.attach_comp]. Two random systems +run [independently in parallel][RandomSystem.parallel], and so do two +[PDC behaviors][PDCBehavior.tensor]. [RandomSystems](src/RandomSystems/README.md) adds automata, +probabilistic automata, memoryless systems and programs. + +**Distance.** The [transcript distance][RandomSystem.transcriptDistance] is the largest +statistical distance of the transcripts that an environment compatible with the domain sees within +$`n`$ queries. It [is the largest advantage][RandomSystem.transcriptDistance_eq_iSup] of a +[probabilistic distinguisher][Domain.Distinguisher] $`P`$ [1, Definition 9]: ```math -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] . +\Delta(R, S) = \sup_{E,\, n}\ \delta\big(\mathrm{tr}(R, E, n),\ \mathrm{tr}(S, E, n)\big) += \sup_P\ \big\lvert \Pr[P(R) = 1] - \Pr[P(S) = 1] \big\rvert . ``` -**Identical until bad** is proved in two layers. At the systems level, two random systems $`R_1`$ -and $`R_2`$ have transcript probabilities that both lie above a common part $`g`$ with -$`g([]) = 1`$. A step from a possible transcript $`h`$ by an admitted query $`x`$ loses -$`g(h) - \sum_y g(h, x, y)`$ of the common part. If each step loses at most -$`\beta(h, x)\, R_1(h)`$, and the [cost][transcriptCost] of each possible transcript, the sum of -$`\beta`$ over its steps, is at most $`\varepsilon`$, then by the union bound over the steps every -compatible environment [stays in the common part][RandomSystem.one_sub_le_sum_tSupp] with -probability at least $`1 - \varepsilon`$, and the two systems are -[within][RandomSystem.transcriptDistance_le_of_transcriptCost_le] $`\varepsilon`$ of each other: - -```math -g(h) - \sum_y g(h, x, y) \le \beta(h, x)\, R_1(h), \qquad -\sum_{k < |h|} \beta(h_1 \cdots h_k,\ x_{k+1}) \le \varepsilon -\quad \Longrightarrow \quad -\Delta(R_1, R_2) \le \varepsilon . -``` - -Games are on top of this. 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][Domain.Distinguisher.winProbability_le_of_transcriptCost_le] -$`\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][RandomSystem.GameEquivalent.transcriptDistance_visible_le] $`\varepsilon`$ of -each other. Two discrete games are equivalent as games when they are -[coupled][PDG.gameEquivalent_behavior_of_isCoupling]: 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][PDCBehavior.liftMBO] $`\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. CR18 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][PDCBehavior.liftMBO_id], $`\hat{\mathrm{id}} = \mathrm{id}`$, and -[composition][PDCBehavior.liftMBO_comp], $`\widehat{\alpha \beta} = \hat\alpha \hat\beta`$. It -[keeps games games][RandomSystem.MonotoneMBO.attach_liftMBO] and -[commutes with the visible system][RandomSystem.visible_attach_liftMBO], -$`(\hat\alpha G)^- = \alpha\, G^-`$. A winner with $`\alpha`$ absorbed -wins $`G`$ [as the winner wins][RandomSystem.winProbability_attach_liftMBO] $`\hat\alpha G`$ -[3, §4.7.2, equation (4.9)]. A [**solver behavior**][Domain.SolverBehavior] pairs a probabilistic -distinguisher's probability of outputting 1 on each random system with its winning probability -for each game, and [absorbing a PDC][Domain.SolverBehavior.absorb] into a solver behavior gives a -solver behavior. - -**Discrete games** present games, as PDSs present random systems. A [discrete game][PDG] is a -distribution over [deterministic discrete games][DDG], pairs of a DDS and a hidden -[monotone condition][MC] 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][DDG.withMBO] as its MBO, -and a discrete game [presents the game][PDG.behavior] of these systems. Its visible system -[is the behavior of the visible systems][PDG.visible_behavior], and on an admitted query sequence -the MBO [is unset with the probability that the condition does not hold][PDG.unsetProbability_behavior], -so a bound on the condition at the empty and every admitted query sequence -[bounds the probability that the MBO is set][PDG.one_sub_le_unsetProbability_behavior]. The game -is [conditionally equivalent][PDG.conditionallyEquivalent_behavior] to a random system $`S`$ when -the replies with the condition unset factor through $`S`$: - -```math -\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][PDG.ofFunction] is a discrete game, and the game it -presents is [conditionally equivalent to the ideal function][PDG.ofFunction_conditionallyEquivalent] -once, on every fixed query sequence, the answers jointly with the unset condition factor through -the ideal answers. +Couplings, restriction, the H-coefficient technique and identical until bad bound the distance: +see [Distance](src/RandomSystems/Distance/README.md). + +**Games.** A [game][RandomSystem.MonotoneMBO] is a random system whose replies carry a bit, the +MBO, which once set stays set [3, §3.7.1]. Its [visible system][RandomSystem.visible] $`G^-`$ +ignores the MBO [3, Definition 4.18], and the +[winning probability][RandomSystem.winProbability] of a distinguisher is the probability that the +MBO is set when it stops [3, Definition 4.5]. When $`G`$ is +[conditionally equivalent][RandomSystem.ConditionallyEquivalent] to $`T`$, +$`G \mathrel{|\!\equiv} T`$ [3, Definition 4.19], every advantage between $`G^-`$ and $`T`$ +[is at most the winning probability][Domain.Distinguisher.advantage_le_winProbability] +[3, Lemma 4.16 and the proof of Theorem 4.17]. For two games +[equivalent as games][RandomSystem.GameEquivalent], this is the +[fundamental lemma][Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent] +[3, Lemma 4.16], [4, Lemma 7 and Theorem 1 (i)]. A converter acts on a game through its +[MBO-forwarding lift][PDCBehavior.liftMBO]. [Game](src/RandomSystems/Game/README.md) adds the +until-bad bound for games and the games presented by discrete games. --- ## 2. Typed systems *The random systems and converters of §1, typed by interfaces [3, Definitions 3.8, 3.9, 3.17], -[6, §3], [7, Definitions 2.2.1–2.2.2]. Every object of this section is a systems-level object; §3 -uses them as the fields of the instances.* - -### 2.1 Interfaces, typed systems and typed converters +[6, §3], [7, Definitions 2.2.1–2.2.2].* An [**interface**][Interface] $`A = (I, X, Y, D)`$ has finitely many labels, finite alphabets $`X_i, Y_i`$, and a domain $`D`$ of input histories, prefix-closed, without the empty history, of -bounded length. Two domains recur: the [**query budget**][Interface.queryBudget] -$`D = \lbrace h \ne \varepsilon \mid \lvert h \rvert \le q \rbrace`$ and the -[**per-port budget**][Interface.portBudget] -$`D = \lbrace h \ne \varepsilon \mid \forall i.\ \lvert h \restriction i \rvert \le q_i \rbrace`$, -where $`h \restriction i`$ [keeps the inputs at the label][restrict] $`i`$. - -A [**typed system**][TypedSystem] on $`A`$ is a random system on +bounded length. A [**typed system**][TypedSystem] on $`A`$ is a random system on $`(\Sigma_i X_i, \Sigma_i Y_i)`$ over $`D`$, [replying at the queried label][RandomSystem.RepliesAtQueriedInterface]. A [**typed converter**][TypedConverter] from $`A`$ to $`B`$ is a PDC behavior from $`B`$'s domain -(inside) to $`A`$'s domain (outside), and a DDC between the two domains -[is one][TypedConverter.ofDDC]. Typed converters compose by the [serial composition][TypedConverter.comp] -of PDC behaviors, with the [identity][TypedConverter.id] PDC behavior. -[**Attachment**][TypedConverter.attach] $`\alpha R`$ is the attachment of the PDC behavior: -[the identity leaves a typed system unchanged][TypedConverter.identity_attach], and -[a serial composition attaches its inner converter first][TypedConverter.comp_smul]. - -[**Parallel interfaces**][Interface.tensor] put the label sets side by side, and -[parallel typed systems][TypedSystem.parallel] and [parallel typed converters][TypedConverter.parallel] -are the independent parallel compositions; attachment [is local][TypedConverter.parallel_attach], -$`(\alpha \otimes \beta)(R \parallel S) = \alpha R \parallel \beta S`$. A label-preserving -bijection of interfaces gives a [**renaming**][TypedConverter.rename], which -[relabels the transcripts][TypedConverter.rename_mass] of the typed system it is attached to; -renamings [compose][TypedConverter.rename_comp], and the renaming by the identity -[is the identity][TypedConverter.rename_refl]. Regrouping three parallel typed systems -[keeps the probabilities][TypedSystem.parallel_assoc_mass] of the regrouped transcripts, the -[dummy system][TypedSystem.dummy] on the [interface without labels][Interface.unit] beside a typed -system keeps its probabilities, on the [left][TypedSystem.parallel_unit_left_mass] and on the -[right][TypedSystem.parallel_unit_right_mass], and [exchanging the two components][TypedSystem.parallel_swap_mass] -of a parallel composition exchanges the labels of its transcripts. The regrouping renamings are -natural for typed converters: [associativity][TypedConverter.comp_associator] and the -[left][TypedConverter.comp_leftUnitor] and [right][TypedConverter.comp_rightUnitor] unit -regroupings commute with parallel typed converters. - -### 2.2 Filters, contexts, sources and functional systems - -The [**filter**][TypedConverter.filter] admitting $`D`$ forwards the queries of admitted histories; -it is a typed converter $`(A \restriction D) \to A`$ from the [restricted interface][Interface.restrict]. -[Attached to a typed system][TypedConverter.filter_smul], it is the -[restriction][RandomSystem.restrict] of the system's random system to the restricted domain, and -[two filters in series][TypedConverter.filter_comp_filter_smul] act as the filter of both -conditions. A [**constant**][TypedConverter.constant] converter ignores its inside system and -exposes a fixed one, and the fixed [right][TypedConverter.rightContext] and -[left][TypedConverter.leftContext] **contexts** run a typed system beside: -[attaching][TypedConverter.attach_rightContext] $`\mathrm{rightContext}\ A\ S`$ to $`R`$ -gives $`R \parallel S`$, and so does [attaching][TypedConverter.attach_leftContext] -$`\mathrm{leftContext}\ R\ B`$ to $`S`$. +(inside) to $`A`$'s domain (outside). Typed converters compose by the +[serial composition][TypedConverter.comp] of PDC behaviors, with the [identity][TypedConverter.id], +and [attachment][TypedConverter.attach] $`\alpha R`$ is the attachment of PDC behaviors. -A [**source**][TypedSystem.source] answers with fresh independent samples of a law: a -memoryless source [3, Definition 3.1] (the sources of [4, Definition 1] may have memory). An -[**automaton**][TypedSystem.ofAutomaton] is a transition function with a sampled initial state -[4, Definition 2], and [parallel automata][TypedSystem.parallel_ofAutomaton] are the automaton -running both side by side. A source [is memoryless][TypedSystem.source_eq_memoryless], -memoryless systems [side by side are memoryless][TypedSystem.parallel_eq_memoryless], and the -converter of a program [maps a memoryless system to the memoryless system of its reply -law][TypedConverter.ofProgram_smul_memoryless], also -[for port-preserving programs][TypedConverter.ofPreservingProgram_smul_memoryless] and -[with its own sources beside its inside interface][TypedConverter.ofPreservingProgram_comp_rightContext_smul_memoryless]: -the composition law of §1.3 on their random systems. **Functional systems** are given by -[reply functions][TypedSystem.ofFunction], by -[conditional reply laws][TypedSystem.ofConditional], or by -[sampling once][TypedSystem.sample] and keeping the sample. +[Parallel interfaces][Interface.tensor] put the label sets side by side. +[Parallel typed systems][TypedSystem.parallel] and [parallel typed converters][TypedConverter.parallel] +are the independent parallel compositions, and attachment [is local][TypedConverter.parallel_attach]: -### 2.3 Typed games +```math +(\alpha \otimes \beta)(R \parallel S) = \alpha R \parallel \beta S . +``` -A [**typed game**][TypedGame] on $`A`$ is a typed system on the [interface][Interface.withMBO] of -$`A`$ with the MBO whose MBO, once set, stays set: a game in the sense of §1.5. A typed converter -[attaches][TypedConverter.attachGame] to it through its [MBO-forwarding lift][PDCBehavior.liftMBO], -and its [visible typed system][TypedGame.visible] is its visible system. A discrete game whose -visible systems present a typed system $`R`$ [presents a typed game][TypedGame.ofPDG] on the -interface of $`R`$, with [visible typed system][TypedGame.visible_ofPDG] $`R`$. A single-label -sampled function with a hidden condition [presents a typed game][TypedGame.ofSingleFunction] -whose random system is [conditionally equivalent][TypedGame.ofSingleFunction_conditionallyEquivalent] -to that of the typed system sampling the ideal function, under the fixed-query factorization. +A label-preserving bijection of interfaces gives a [renaming][TypedConverter.rename], and the +renamings regroup parallel compositions. A [**typed game**][TypedGame] on $`A`$ is a typed system +on the interface of $`A`$ with the MBO whose MBO, once set, stays set. +[Typed](src/RandomSystems/Typed/README.md) adds budgets, the coherence laws of parallel +composition, filters, contexts, sources, automata, memoryless and functional systems, and the +typed games presented by discrete games. --- -## 3. The abstract layers and their instances +## 3. Classes and instances *Each layer is a class of assumptions: it introduces its notions (attachment, parallel composition, distance, distinguishers, games, winners, solvers) only as fields and axioms, and -knows nothing about systems [3, §§4.4.3, 4.5.1, 4.7.2, 4.10–4.11], [6, §3], [7, §2.2], [8]. Interfaces -are an instance of each class: the carrier $`\Phi A`$ is the typed systems on $`A`$, every field is -a systems-level object of §1–2, and every axiom is discharged by a systems-level theorem. Only the -classes say "resource", for an element of $`\Phi A`$.* +knows nothing about systems [3, §§4.4.3, 4.5.1, 4.7.2, 4.10–4.11], [6, §3], [7, §2.2], [8]. +Interfaces are an instance of each class: the carrier $`\Phi A`$ is the typed systems on $`A`$, +every field is a systems-level object of §1–2, and every axiom is discharged by a systems-level +theorem. Only the classes say "resource", for an element of $`\Phi A`$.* ``` Category ─▶ MonoidalCategory @@ -440,225 +137,70 @@ ResourceTheory ─▶ CryptographicAlgebra ─▶ CompatiblePseudoMetric ─▶ Games ─▶ DistinctionGames ``` -### 3.1 The category of interfaces - -Interfaces and typed converters form a category under serial composition, and a monoidal -category under parallel composition. - -Interfaces are an instance of Mathlib's `Category` ([`Interface.category`][Interface.category]) -with the interfaces as objects: its field `Hom A B` is [`TypedConverter A B`][TypedConverter], -`id` is [`TypedConverter.id`][TypedConverter.id] and `comp` is -[`TypedConverter.comp`][TypedConverter.comp], the identity and the serial composition of PDC -behaviors; the axioms `id_comp`, `comp_id` and `assoc` are discharged by the -[left identity][PDCBehavior.id_comp], [right identity][PDCBehavior.comp_id] and -[associativity][PDCBehavior.comp_assoc] laws of PDC behaviors. - -Interfaces are an instance of `MonoidalCategory` ([`Interface.monoidal`][Interface.monoidal], -on the structure [`Interface.monoidalStruct`][Interface.monoidalStruct]): `tensorObj` is the -[parallel interface][Interface.tensor], `tensorHom` is -[`TypedConverter.parallel`][TypedConverter.parallel], the parallel composition of PDC behaviors, -the unit is the [interface without labels][Interface.unit], and the -[associator][Interface.associator] and the [left][Interface.leftUnitor] and -[right][Interface.rightUnitor] unitors are the [isomorphisms][Interface.isoOf] of the regrouping -[renamings][TypedConverter.rename], with inverses by [`TypedConverter.rename_comp`][TypedConverter.rename_comp] -and [`TypedConverter.rename_refl`][TypedConverter.rename_refl]. The axioms are discharged by -[interchange][Interface.tensor_comp], from the -[interchange of PDC behaviors][PDCBehavior.comp_tensor]; the -[tensor of identities][Interface.id_tensor_id], from the -[same law for PDC behaviors][PDCBehavior.tensor_id]; the -[naturality of the associator][Interface.associator_naturality], from the systems-level -[naturality of the associativity renaming][TypedConverter.comp_associator]; the naturality of the -[left][Interface.leftUnitor_naturality] and [right][Interface.rightUnitor_naturality] unitors, -from the [left][TypedConverter.comp_leftUnitor] and [right][TypedConverter.comp_rightUnitor] unit -renamings; and the [pentagon][Interface.pentagon] and [triangle][Interface.triangle] identities, -from [parallel renamings][TypedConverter.parallel_rename] and their composition. - -### 3.2 `ResourceTheory C Φ`: attachment - -In the class [`ResourceTheory`][ResourceTheory], converters $`\alpha : A \to B`$ act on resources -$`R \in \Phi B`$: - -```math -\alpha R \in \Phi A, \qquad \mathrm{id}_A\, R = R, \qquad (\alpha \gg \beta)\, R = \alpha\,(\beta\, R) . -``` - -Attachment is the [contravariant functor][ResourceTheory.functor] -$`\Phi : C^{\mathrm{op}} \to \mathrm{Type}`$. - -Interfaces are an instance of `ResourceTheory` -([`Interface.resourceTheory`][Interface.resourceTheory]) with carrier -$`\Phi A :=`$ [`TypedSystem A`][TypedSystem]: its field `attach` is -[`TypedConverter.attach`][TypedConverter.attach], the systems-level -[attachment of PDC behaviors][PDCBehavior.attach]; its axioms `attach_identity` and -`attach_serial` are discharged by [`TypedConverter.identity_attach`][TypedConverter.identity_attach] -and [`TypedConverter.comp_smul`][TypedConverter.comp_smul], from the -[identity][PDCBehavior.attach_id] and [serial][PDCBehavior.attach_comp] attachment laws of PDC -behaviors. In the notation of the category they read [`Interface.identity_attach`][Interface.identity_attach] -and [`Interface.comp_smul`][Interface.comp_smul]. - -### 3.3 `CryptographicAlgebra C Φ`: parallel composition - -The class [`CryptographicAlgebra`][CryptographicAlgebra] is a lax monoidal structure on $`\Phi`$: -resources [compose in parallel][CA.parallel], with the [dummy resource][CA.dummy] as unit. - -```math -R \parallel S \in \Phi(A \otimes B), \qquad \mathbf 1 \in \Phi(\mathbb I), \qquad -(\alpha \otimes \beta)(R \parallel S) = \alpha R \parallel \beta S . -``` - -Derived: [locality][CA.attach_parallel], [associativity][CA.parallel_assoc], and the -[left][CA.parallel_dummy_left] and [right][CA.parallel_dummy_right] unit laws. - -Interfaces are an instance of `CryptographicAlgebra` -([`Interface.cryptographicAlgebra`][Interface.cryptographicAlgebra]) with carrier -$`\Phi A :=`$ `TypedSystem A`: its field `laxMonoidal` is -[`Interface.resourcesLaxMonoidal`][Interface.resourcesLaxMonoidal], whose product is -[`TypedSystem.parallel`][TypedSystem.parallel], the systems-level -[independent parallel composition][RandomSystem.parallel], and whose unit is the -[dummy typed system][TypedSystem.dummy]. Naturality is discharged by the -[locality of attachment][TypedConverter.parallel_attach]; associativity and unitality by -[`Interface.parallel_assoc`][Interface.parallel_assoc] and the -[left][Interface.parallel_dummy_left] and [right][Interface.parallel_dummy_right] unit laws, -which are the systems-level [regrouping][TypedSystem.parallel_assoc_mass] and -[left][TypedSystem.parallel_unit_left_mass] and [right][TypedSystem.parallel_unit_right_mass] unit -laws of parallel typed systems, read through the [renaming][TypedConverter.rename_mass] of the -regrouping isomorphisms. The abstract [parallel composition][Interface.cc_parallel_eq] and -[dummy][Interface.cc_dummy_eq] are the systems-level ones. - -### 3.4 `CompatiblePseudoMetric C Φ`: distance - -The class [`CompatiblePseudoMetric`][CompatiblePseudoMetric] adds a pseudo-metric $`d`$, the -[distance][CA.distance], on each $`\Phi A`$ [6, Definition 2], [8, Definition 2]: - -```math -d(\alpha R, \alpha S) \le d(R, S), \qquad -d(R \parallel R',\ S \parallel S') \le d(R, S) + d(R', S') . -``` - -Derived: [attachment is non-expanding][distance_attach_le] and -[parallel composition adds distances][distance_parallel_le]. For interfaces the metric comes from -the distinguisher class below. - -### 3.5 `CompatibleDistinguisherClass C Φ`: distinguishers - -The class [`CompatibleDistinguisherClass`][CompatibleDistinguisherClass] has a class -$`\mathcal D_A`$ of maps $`\Phi A \to \mathbb R`$, closed under absorbing a converter and under running -a fixed resource beside, whose [advantage distance][advantageDistance] is the metric [8, §4.5]: - -```math -d(R, S) = \sup_{D \in \mathcal D_A} \lvert D(R) - D(S) \rvert, \qquad -D \in \mathcal D_A \;\Longrightarrow\; D(\alpha\,\cdot\,) \in \mathcal D_B,\ \ D(\,\cdot \parallel T),\ D(T \parallel \cdot\,) \in \mathcal D . -``` - -**Closure gives compatibility** [8, Lemma 1]: the advantage distance of a closed class -[is a compatible pseudo-metric][CompatibleDistinguisherClass.ofClosure]. - -Interfaces are an instance of `CompatibleDistinguisherClass` -([`Interface.compatibleDistinguisherClass`][Interface.compatibleDistinguisherClass], built by -`ofClosure`) with carrier $`\Phi A :=`$ `TypedSystem A`: its field `distinguishers A` is the -[set of maps][Interface.distinguishers] $`R \mapsto \Pr[d(R) = 1]`$ for the systems-level -[distinguisher behaviors][Domain.DistinguisherBehavior] $`d`$ compatible with $`A`$'s domain. Its -axiom `closed_attach` is discharged by [closure under attachment][Interface.distinguishers_attach], -from [absorbing a converter][DistinguisherBehavior.absorb]; `closed_parallel_left` by -[closure under a typed system run on the right][Interface.distinguishers_parallel_left], from -[absorbing a system run beside][Domain.Distinguisher.exists_absorbRight]; and -`closed_parallel_right` by -[closure under a typed system run on the left][Interface.distinguishers_parallel_right], from the -previous two through the [swap][Interface.parallel_swap], the [isomorphism][Interface.swap] of the -renaming that [exchanges the two components][TypedSystem.parallel_swap_mass]. Its metric -[is the transcript distance][Interface.cc_distance_eq] of §1.4: - -```math -d(R, S) = \Delta(R, S) = \sup_P \mathrm{Adv}_P(R, S) . -``` - -### 3.6 `Games C Game` and `DistinctionGames C Φ Game`: games, and games related to distinguishing - -The class [`Games`][Games] is the abstraction of [3, §4.4.3, §4.5.1 and §4.7.2]. A problem is a -set of solvers with a performance function [3, Definition 4.2]; for a game the solvers are -winners and the performance is the winning probability [3, Definition 4.5], so a winner is given -by its winning probability $`W : \mathrm{Game}\,A \to \mathbb R`$ for each game. The class has games -$`\mathrm{Game}\,A`$ on each object, attachment $`\alpha \cdot G`$ of converters to games, -contravariant in serial composition, and a set $`\mathcal W_A`$ of winners closed under -[absorbing][Games.absorb] a converter, $`\omega(w c, g) = \omega(w, c g)`$ [3, §4.7.2, -equation (4.9)]. Games and winners do not involve resources: - -```math -\mathrm{id} \cdot G = G, \qquad (\alpha \beta) \cdot G = \alpha \cdot (\beta \cdot G), \qquad -W \in \mathcal W_A \;\Longrightarrow\; W(\alpha \cdot\,\cdot\,) \in \mathcal W_B . -``` - -Absorbing a serial composition [absorbs its converters in turn][Games.absorb_comp]. - -The class [`DistinctionGames`][DistinctionGames], extending `Games`, is the abstraction of -[3, §§4.10–4.11], relating games and distinction problems. Its solvers are the objects that are -both a distinguisher and a winner, as $`D`$ in [3, Lemma 4.16]: a set $`\mathcal S_A`$ of pairs -$`(D, W)`$ of a decision probability $`D : \Phi A \to \mathbb R`$ and a winning probability $`W`$, which -is a winner, closed under [absorbing][DistinctionGames.absorb] a converter [3, §4.7.2]. It has the visible -resource $`G^-`$ of a game [3, Definition 4.18], with which attachment commutes since a converter -neither sees nor affects the MBO [3, §4.7.2], and a conditional equivalence -$`G \mathrel{|\!\equiv} T`$ of games to resources [3, Definition 4.19], under which each solver's advantage is at most its winning -probability [3, Lemma 4.16 and the proof of Theorem 4.17]: - -```math -(D, W) \in \mathcal S_A \;\Longrightarrow\; W \in \mathcal W_A, \qquad -(\alpha \cdot G)^- = \alpha\, G^-, \qquad -G \mathrel{|\!\equiv} T,\ (D, W) \in \mathcal S_A \;\Longrightarrow\; \lvert D(G^-) - D(T) \rvert \le W(G) . -``` - -Interfaces are an instance of both classes, and the instance is the only place where they meet -random systems: its games are the typed games of §2.3, MBO random systems as [3, §3.7.1] -instantiates games, and its winners and solvers are probabilistic distinguishers, through their -[solver behaviors][Domain.SolverBehavior]. - -Interfaces are an instance of `Games` ([`Interface.games`][Interface.games]): its field `Game A` -is [`TypedGame A`][TypedGame], the typed systems on the interface of $`A`$ with the MBO whose MBO, -once set, stays set ([`RandomSystem.MonotoneMBO`][RandomSystem.MonotoneMBO]); `attachGame` is -[`TypedConverter.attachGame`][TypedConverter.attachGame], the attachment of the systems-level -[lift][PDCBehavior.liftMBO] of the converter; and `winners A` is the set of -[winning probabilities][Interface.winners] of the systems-level solver behaviors on $`A`$'s -domain. Its axiom `attachGame_identity` is discharged by -[`PDCBehavior.liftMBO_id`][PDCBehavior.liftMBO_id], `attachGame_serial` by -[`PDCBehavior.liftMBO_comp`][PDCBehavior.liftMBO_comp], and `closed_attach` by -[absorbing a PDC into a solver behavior][Domain.SolverBehavior.absorb]. A bound on the winning -probability of every distinguisher -[bounds the winning probability of every winner][Interface.win_le]. - -Interfaces are an instance of `DistinctionGames` -([`Interface.distinctionGames`][Interface.distinctionGames]) with carrier $`\Phi A :=`$ -`TypedSystem A` and games `TypedGame A`: its field `solvers A` is the -[set of pairs][Interface.solvers] of the solver behaviors on $`A`$'s domain, `visible` is -[`TypedGame.visible`][TypedGame.visible], the systems-level [visible system][RandomSystem.visible], -and `ConditionallyEquivalent` is the systems-level -[conditional equivalence][RandomSystem.ConditionallyEquivalent] of the random systems. Its axiom -`solvers_winner` holds by the definition of the winners, `solvers_closed_attach` is discharged by -[`Domain.SolverBehavior.absorb`][Domain.SolverBehavior.absorb], `visible_attachGame` by -[`RandomSystem.visible_attach_liftMBO`][RandomSystem.visible_attach_liftMBO], and -`advantage_le_win` by -[`Domain.Distinguisher.advantage_le_winProbability`][Domain.Distinguisher.advantage_le_winProbability]. -A typed game conditionally equivalent to a typed system $`T`$, $`G \mathrel{|\!\equiv} T`$, whose MBO -stays unset with probability at least $`1 - \varepsilon`$ on fixed queries, -[has its visible typed system within][Interface.dist_visible_le] $`\varepsilon`$ of $`T`$, -$`\Delta(G^-, T) \le \varepsilon`$ [3, Theorem 4.17]. A presented typed game is conditionally -equivalent to a typed system [exactly when][Interface.conditionallyEquivalent_ofPDG_iff] the game -it presents on random systems is; if it is conditionally equivalent to $`S`$ and the condition -holds with probability at most $`\varepsilon`$ on the empty and every admitted query sequence, the -presented typed system $`R`$ is [within][Interface.game_dist_le] $`\varepsilon`$ of $`S`$, -$`\Delta(R, S) \le \varepsilon`$. - -**Notation** (`open scoped SystemAlgebra`): [`Δ R S`][notation-distance] for the distance of -§3.4, [`R ∥ S`][notation-parallel] for `TypedSystem.parallel`, -[`𝓡 —[π]→ 𝒮`][notation-constructs] for $`\mathcal R \xrightarrow{\pi} \mathcal S`$ and -[`𝓡 —[π; ε]→ 𝒮`][notation-constructsWithin] for -$`\mathcal R \xrightarrow{\pi,\ \varepsilon} \mathcal S`$ (§4), and -[`G |≡ T`][notation-conditionallyEquivalent] for $`G \mathrel{|\!\equiv} T`$. +The table gives each class with its instance on interfaces, each field with the systems-level +object that fills it, and each axiom with the systems-level theorem that discharges it. +[ConstructiveCryptography](src/ConstructiveCryptography/README.md) states the classes, their +derived laws, and the consequences of the instances. + +| Class, instance | Field or axiom | Systems level | +|---|---|---| +| `Category` (Mathlib), [`Interface.category`][Interface.category] | objects | [interfaces][Interface] | +| | `Hom A B` | [`TypedConverter A B`][TypedConverter] | +| | `id`, `comp` | [`TypedConverter.id`][TypedConverter.id], [`TypedConverter.comp`][TypedConverter.comp]: the identity and the serial composition of PDC behaviors | +| | `id_comp`, `comp_id`, `assoc` | [`PDCBehavior.id_comp`][PDCBehavior.id_comp], [`PDCBehavior.comp_id`][PDCBehavior.comp_id], [`PDCBehavior.comp_assoc`][PDCBehavior.comp_assoc] | +| `MonoidalCategory` (Mathlib), [`Interface.monoidal`][Interface.monoidal] by `MonoidalCategory.ofTensorHom` on [`Interface.monoidalStruct`][Interface.monoidalStruct] | `tensorObj`, `tensorUnit` | [`Interface.tensor`][Interface.tensor], [`Interface.unit`][Interface.unit] | +| | `tensorHom` | [`TypedConverter.parallel`][TypedConverter.parallel], the parallel composition of PDC behaviors; `whiskerLeft` and `whiskerRight` are it with an identity | +| | `associator`, `leftUnitor`, `rightUnitor` | [`Interface.associator`][Interface.associator], [`Interface.leftUnitor`][Interface.leftUnitor], [`Interface.rightUnitor`][Interface.rightUnitor]: the [isomorphisms][Interface.isoOf] of the regrouping [renamings][TypedConverter.rename], with inverses by [`TypedConverter.rename_comp`][TypedConverter.rename_comp] and [`TypedConverter.rename_refl`][TypedConverter.rename_refl] | +| | `id_tensorHom_id` ([`Interface.id_tensor_id`][Interface.id_tensor_id]) | [`PDCBehavior.tensor_id`][PDCBehavior.tensor_id] | +| | `id_tensorHom`, `tensorHom_id` | the definition of the whiskers | +| | `tensorHom_comp_tensorHom`, interchange ([`Interface.tensor_comp`][Interface.tensor_comp]) | [`PDCBehavior.comp_tensor`][PDCBehavior.comp_tensor] | +| | `associator_naturality` ([`Interface.associator_naturality`][Interface.associator_naturality]) | [`TypedConverter.comp_associator`][TypedConverter.comp_associator] | +| | `leftUnitor_naturality`, `rightUnitor_naturality` ([left][Interface.leftUnitor_naturality], [right][Interface.rightUnitor_naturality]) | [`TypedConverter.comp_leftUnitor`][TypedConverter.comp_leftUnitor], [`TypedConverter.comp_rightUnitor`][TypedConverter.comp_rightUnitor] | +| | `pentagon`, `triangle` ([`Interface.pentagon`][Interface.pentagon], [`Interface.triangle`][Interface.triangle]) | [`TypedConverter.parallel_rename`][TypedConverter.parallel_rename] and [`TypedConverter.rename_comp`][TypedConverter.rename_comp] | +| [`ResourceTheory`][ResourceTheory]: attachment; [`Interface.resourceTheory`][Interface.resourceTheory] | carrier $`\Phi A`$ | [`TypedSystem A`][TypedSystem] | +| | `attach` | [`TypedConverter.attach`][TypedConverter.attach], the [attachment of PDC behaviors][PDCBehavior.attach] | +| | `attach_identity` | [`TypedConverter.identity_attach`][TypedConverter.identity_attach], from [`PDCBehavior.attach_id`][PDCBehavior.attach_id] | +| | `attach_serial` | [`TypedConverter.comp_smul`][TypedConverter.comp_smul], from [`PDCBehavior.attach_comp`][PDCBehavior.attach_comp] | +| [`CryptographicAlgebra`][CryptographicAlgebra]: parallel composition; [`Interface.cryptographicAlgebra`][Interface.cryptographicAlgebra] | `laxMonoidal` | [`Interface.resourcesLaxMonoidal`][Interface.resourcesLaxMonoidal] | +| | its product `μ` | [`TypedSystem.parallel`][TypedSystem.parallel], the [independent parallel composition][RandomSystem.parallel] ([`Interface.cc_parallel_eq`][Interface.cc_parallel_eq]) | +| | its unit `ε` | the [dummy typed system][TypedSystem.dummy] ([`Interface.cc_dummy_eq`][Interface.cc_dummy_eq]) | +| | `μ_natural_left`, `μ_natural_right` | [`TypedConverter.parallel_attach`][TypedConverter.parallel_attach], the locality of attachment | +| | `associativity` ([`Interface.parallel_assoc`][Interface.parallel_assoc]) | [`TypedSystem.parallel_assoc_mass`][TypedSystem.parallel_assoc_mass], through [`TypedConverter.rename_mass`][TypedConverter.rename_mass] | +| | `left_unitality`, `right_unitality` ([left][Interface.parallel_dummy_left], [right][Interface.parallel_dummy_right]) | [`TypedSystem.parallel_unit_left_mass`][TypedSystem.parallel_unit_left_mass], [`TypedSystem.parallel_unit_right_mass`][TypedSystem.parallel_unit_right_mass], through [`TypedConverter.rename_mass`][TypedConverter.rename_mass] | +| [`CompatiblePseudoMetric`][CompatiblePseudoMetric]: distance; through [`Interface.compatibleDistinguisherClass`][Interface.compatibleDistinguisherClass] | `fibreMetric` | the [advantage distance][advantageDistance] of the distinguishers below, which [is the transcript distance][Interface.cc_distance_eq] | +| | `edist_smul_le`, `edist_parallel_le` | [`CompatibleDistinguisherClass.ofClosure`][CompatibleDistinguisherClass.ofClosure] [8, Lemma 1], from the closure axioms below | +| [`CompatibleDistinguisherClass`][CompatibleDistinguisherClass]: distinguishers; [`Interface.compatibleDistinguisherClass`][Interface.compatibleDistinguisherClass] by `ofClosure` | `distinguishers A` | [`Interface.distinguishers`][Interface.distinguishers]: the maps $`R \mapsto \Pr[d(R) = 1]`$ for the [distinguisher behaviors][Domain.DistinguisherBehavior] $`d`$ compatible with $`A`$'s domain | +| | `closed_attach` ([`Interface.distinguishers_attach`][Interface.distinguishers_attach]) | [absorbing a converter][DistinguisherBehavior.absorb] | +| | `closed_parallel_left` ([`Interface.distinguishers_parallel_left`][Interface.distinguishers_parallel_left]) | [absorbing a system run beside][Domain.Distinguisher.exists_absorbRight] | +| | `closed_parallel_right` ([`Interface.distinguishers_parallel_right`][Interface.distinguishers_parallel_right]) | the previous two, through the [swap][Interface.parallel_swap], the [isomorphism][Interface.swap] of the renaming that [exchanges the two components][TypedSystem.parallel_swap_mass] | +| | `edist_eq` | the definition of the metric in `ofClosure` | +| [`Games`][Games]: games and winners; [`Interface.games`][Interface.games] | `Game A` | [`TypedGame A`][TypedGame]: the typed systems on the interface of $`A`$ with the MBO whose MBO stays set ([`RandomSystem.MonotoneMBO`][RandomSystem.MonotoneMBO]) | +| | `attachGame` | [`TypedConverter.attachGame`][TypedConverter.attachGame], the attachment of the [MBO-forwarding lift][PDCBehavior.liftMBO] | +| | `winners A` | [`Interface.winners`][Interface.winners]: the winning probabilities of the [solver behaviors][Domain.SolverBehavior] on $`A`$'s domain | +| | `attachGame_identity` | [`PDCBehavior.liftMBO_id`][PDCBehavior.liftMBO_id], with [`PDCBehavior.attach_id`][PDCBehavior.attach_id] | +| | `attachGame_serial` | [`PDCBehavior.liftMBO_comp`][PDCBehavior.liftMBO_comp], with [`PDCBehavior.attach_comp`][PDCBehavior.attach_comp] | +| | `closed_attach` | [`Domain.SolverBehavior.absorb`][Domain.SolverBehavior.absorb] | +| [`DistinctionGames`][DistinctionGames]: games and distinguishing; [`Interface.distinctionGames`][Interface.distinctionGames] | carrier, games | `TypedSystem A`, `TypedGame A` | +| | `solvers A` | [`Interface.solvers`][Interface.solvers]: the pairs of the solver behaviors on $`A`$'s domain | +| | `visible` | [`TypedGame.visible`][TypedGame.visible], the [visible system][RandomSystem.visible] | +| | `ConditionallyEquivalent` | [`RandomSystem.ConditionallyEquivalent`][RandomSystem.ConditionallyEquivalent] | +| | `solvers_winner` | the definition of the winners | +| | `solvers_closed_attach` | [`Domain.SolverBehavior.absorb`][Domain.SolverBehavior.absorb] | +| | `visible_attachGame` | [`RandomSystem.visible_attach_liftMBO`][RandomSystem.visible_attach_liftMBO] | +| | `advantage_le_win` | [`Domain.Distinguisher.advantage_le_winProbability`][Domain.Distinguisher.advantage_le_winProbability] | + +So the metric of the instance is the transcript distance of §1, $`d(R, S) = \Delta(R, S)`$, and +a typed game conditionally equivalent to a typed system $`T`$, whose MBO stays unset with +probability at least $`1 - \varepsilon`$ on fixed queries, +[has its visible typed system within][Interface.dist_visible_le] $`\varepsilon`$ of $`T`$ +[3, Theorem 4.17]. --- -## 4. Specifications and constructions +## 4. Constructions and the substitution calculus -*A specification is a set of resources; a converter constructs one specification from another -[6, §§2–4]. The carrier-free notions hold for any map; the others are stated on the classes of §3.* +A [**specification**][Specification] is a set of resources, and a converter $`\pi`$ constructs one +specification from another [6, §§2–4], exactly or within $`\varepsilon`$: ```math \mathcal R \xrightarrow{\ \pi\ } \mathcal S \;:\iff\; \pi\mathcal R \subseteq \mathcal S, @@ -667,249 +209,48 @@ $`\mathcal R \xrightarrow{\pi,\ \varepsilon} \mathcal S`$ (§4), and \forall R \in \mathcal R\ \exists S \in \mathcal S.\ d(\pi R, S) \le \varepsilon . ``` -A [**specification**][Specification] is a set; [exact][Specification.Constructs] and -[approximate][Specification.ConstructsWithin] construction are as above, for any map. On a -cryptographic algebra the map is attachment, giving [exact][CA.Specification.Constructs] and -[approximate][CA.Specification.ConstructsWithin] construction by a converter. Constructions -compose serially [6, Lemma 1], -$`\mathcal R \xrightarrow{\pi_2} \mathcal S \xrightarrow{\pi_1} \mathcal T \Rightarrow \mathcal R \xrightarrow{\pi_1 \gg \pi_2} \mathcal T`$, -[exactly][Constructs.serial] and [approximately][ConstructsWithin.serial] with added errors, and in -parallel, $`\mathcal R \parallel \mathcal R' \xrightarrow{\pi \otimes \pi'} \mathcal S \parallel \mathcal S'`$, -[exactly][Constructs.parallel] and [approximately][ConstructsWithin.parallel]. - -A [**relaxation**][Relaxation] maps each $`R`$ to a set $`\mathcal R' \ni R`$, lifted to -specifications by union. A relaxation is [compatible][Relaxation.Compatible] when -[it preserves construction][Relaxation.compatible_iff], and compatible relaxations -[pass through serial constructions][Constructs.relax_serial]. The -[**ε-relaxation**][epsilonRelaxation] -$`\mathcal R^\varepsilon = \lbrace R' \mid \exists R \in \mathcal R.\ d(R, R') \le \varepsilon \rbrace`$ -[turns approximate construction into exact construction][constructs_epsilonRelaxation_iff], -$`\mathcal R \xrightarrow{\pi} \mathcal S^\varepsilon \iff \mathcal R \xrightarrow{\pi,\ \varepsilon} \mathcal S`$, -and its errors [add under serial composition][Constructs.serial_epsilonRelaxation]. - -The [**star relaxation**][CA.star] [6, §3.4, Lemma 3] -$`\mathcal R^{*} = \lbrace \sigma R \mid \sigma \in \Sigma,\ R \in \mathcal R \rbrace`$ is -[idempotent][star_idem], a [closure operator][starClosure], and -[exact construction survives star-relaxing both ends][Constructs.star] for a converter commuting -with the class. A [**simulator**][constructs_of_simulator] [6, Lemma 5] $`\sigma \in \Sigma`$ with -$`d(\pi R, \sigma S) \le \varepsilon`$ gives -$`\lbrace R \rbrace \xrightarrow{\pi} (\lbrace S \rbrace^{*})^{\varepsilon}`$. Other relaxations and -judgments are the [kernel relaxation][kernel] of a map, [test-bounded specifications][gameSpec], -and [constructibility][Constructible] by a class of constructors. +Constructions compose [serially][ConstructsWithin.serial] [6, Lemma 1] and +[in parallel][ConstructsWithin.parallel], with added errors. A [relaxation][Relaxation] enlarges +a specification, and a simulator [gives a construction][constructs_of_simulator] [6, Lemma 5] of +a relaxed one: its star relaxation [6, §3.4, Lemma 3], within the error of the simulation. + +The **substitution calculus** [9, Chapter 2 and §4.1.4], [7, Definitions 2.2.6–2.2.9 and +Theorem 2.2.10] is stated over any `ResourceTheory`. An [implication witness][Implication] +derives a target substitution from assumptions by a chain of substitutions in contexts +[9, §2.3.1], and counts the uses of each assumption. +[Substitution within an error function][SubstitutesWithin] [9, §2.3.3], $`S \simeq_\varepsilon T`$ +when $`\Delta_D(S, T) \le \varepsilon(D)`$ for every admitted distinguisher $`D`$, transports +through a converter by absorbing it into the distinguishers [9, p. 16], and along a witness the +[assumption uses][Implication.substitutesWithin] and the +[statistical steps][Implication.substitutesWithin_of_mixed] add up [7, Theorem 2.2.10]. On +interfaces the [distinguishing advantage][Interface.distinguisherAdvantage] is the systems-level +advantage of distinguisher behaviors, and every security notion of Commons is a substitution +$`R \simeq_\varepsilon S`$ for it. Relaxations, simulators and the rest of the calculus are in +[ConstructiveCryptography](src/ConstructiveCryptography/README.md). --- -## 5. The substitution calculus - -*Stated over any [`ResourceTheory`][ResourceTheory] [9, Chapter 2 and §4.1.4], -[7, Definitions 2.2.6–2.2.9 and Theorem 2.2.10].* +## 5. The DSL, the proof commands and the examples -### 5.1 Substitution relations and implication witnesses +**DSL.** `interface`, `system`, `converter` and `filter` declarations compile to the typed systems +and typed converters of §2 at every budget ([DSL][DSL]); converters are arrows of the category of +interfaces, so that components assemble with `≫` and `⊗ₘ`. A component compiles to a +deterministic [program][Program] and [sources][TypedSystem.source] of fresh samples, and compiled +components are automata, compared by [bisimulation][automatonSystem_eq_of_bisim]. The syntax and +what each declaration generates are in [GRAMMAR][Grammar]. -A [**substitution relation**][SubstitutionRelation] $`\simeq`$ relates resources on one -interface [9, Definition 2.3.1]: - -```math -S \simeq T \Rightarrow T \simeq S, \qquad S \simeq T \simeq U \Rightarrow S \simeq U, \qquad -S \simeq T \Rightarrow \rho S \simeq \rho T . -``` - -An [**implication witness**][Implication] from assumptions $`S_i \simeq T_i`$ to a target -$`X \simeq Y`$ is a chain [9, §2.3.1]: - -```math -X = \rho_0 S_{i_0}^{b_0} \simeq \rho_0 S_{i_0}^{\lnot b_0} = \rho_1 S_{i_1}^{b_1} \simeq \cdots \simeq \rho_k S_{i_k}^{\lnot b_k} = Y . -``` +**Proof commands.** [`cc_normalize`][cc_normalize] rewrites attachments to normal forms, +[`cc_nonexpand`][cc_nonexpand] applies the compatibility laws, [`cc_triangle`][cc_triangle] takes +a hybrid step, [`cc_construct`][cc_construct] reduces a construction to its equality or distance +obligation, and [`cc_calc`][cc_calc] proves substitutions and distances by chains of steps. They +are described in [GRAMMAR](src/ConstructiveCryptography/DSL/GRAMMAR.md#proof-commands). -A witness [counts the uses][Implication.usageCount] of each assumption. The hybrid argument -[9, Lemma 2.3.2] holds [for a substitution relation][substitutes_of_hybrid] and -[for distances][distance_hybrid_le]. A witness [is valid][Implication.substitutes], taking valid -assumptions to its target, and [distances add][Implication.distance_le] along it. Witnesses can be -[transformed by a converter][Implication.map], [reversed][Implication.reverse] and -[appended][Implication.append], and [use counts add][usageCount_append] under appending. The -derivable targets form the [generated relation][generatedRelation], and they -[hold in every substitution relation satisfying the assumptions][derivable_substitutes]. - -### 5.2 Distinguisher-indexed substitution - -A [**distinguisher advantage**][DistinguisherAdvantage] gives admitted distinguishers -$`\mathcal D_A`$ and an advantage $`\Delta_D`$, a pseudo-distance for each $`D`$. -[Substitution within an error *function*][SubstitutesWithin] [9, §2.3.3]: - -```math -S \simeq_{\varepsilon} T \;:\iff\; \forall D \in \mathcal D_A.\ \Delta_D(S, T) \le \varepsilon(D) . -``` - -Substitution is [symmetric][SubstitutesWithin.symm], and [errors add][SubstitutesWithin.trans]: -$`S \simeq_\varepsilon T \simeq_{\varepsilon'} U \Rightarrow S \simeq_{\varepsilon + \varepsilon'} U`$. -A statistical step gives a substitution within a constant error, -[from a distance bound][SubstitutesWithin.of_distance] $`d(S, T) \le \varepsilon`$ when -$`\Delta_D \le d`$, and more generally -[from any statistical bound dominating the advantage][SubstitutesWithin.of_statistical]. Reduction [9, p. 16], -$`S \simeq_\varepsilon T \Rightarrow \rho S \simeq_{\varepsilon(\cdot \circ \rho)} \rho T`$, -transports substitutions [through one converter][SubstitutesWithin.attach] and -[through a serial composition][SubstitutesWithin.attach_serial]. In mixed chains -[7, Theorem 2.2.10], the [assumption uses][Implication.substitutesWithin] and the -[statistical steps][Implication.substitutesWithin_of_mixed] along a witness add up. - -**On interfaces.** [`DistinguisherAdvantage`][DistinguisherAdvantage] is a structure, and for every -class of admitted distinguishers [`Interface.distinguisherAdvantage`][Interface.distinguisherAdvantage] -is one, with carrier $`\Phi A :=`$ `TypedSystem A`: its distinguishers are the systems-level -[distinguisher behaviors][Domain.DistinguisherBehavior], its field `admissible` is that class, its -field `advantage` is the systems-level -[advantage][DistinguisherBehavior.advantage], and its laws `advantage_self`, `advantage_symm` and -`advantage_triangle` are the systems-level [zero][DistinguisherBehavior.advantage_self], -[symmetry][DistinguisherBehavior.advantage_symm] and -[triangle][DistinguisherBehavior.advantage_triangle] laws. - -A converter $`\alpha`$ absorbed into a distinguisher is the reduction of a security proof [3]: -the systems-level [absorption][DistinguisherBehavior.absorb] gives $`D \circ \alpha`$, and absorbing -a serial composition [absorbs its converters in turn][DistinguisherBehavior.absorb_comp], -$`D \circ (\alpha \gg \beta) = (D \circ \alpha) \circ \beta`$. Hence an advantage between attachments -[is the advantage with the converter absorbed][Interface.distinguisherAdvantage_attach], -$`\mathrm{Adv}_D(\alpha R, \alpha S) = \mathrm{Adv}_{D \circ \alpha}(R, S)`$; every advantage -[is at most the distance][Interface.distinguisherAdvantage_le_distance], $`\mathrm{Adv}_D \le \Delta`$, -by the [systems-level bound][DistinguisherBehavior.advantage_le_transcriptDistance]; and -substitutions [transport through converters][Interface.substitutesWithin_attach] when the class is -closed under absorbing converters. The class -[`Interface.AdmissibleDistinguishers`][Interface.AdmissibleDistinguishers] -bundles the admitted distinguishers with that closure; for its instance in scope, -$`R \simeq_\varepsilon S`$ is written [`R ≃[ε] S`][notation-substitutes] (scoped in -`SystemAlgebra`), substitutions -[transport through every converter][AdmissibleDistinguishers.substitutesWithin_attach], and every -security notion of Commons is stated this way. - -### 5.3 Substitution relaxations and constructions - -The [**substitution image**][substitutionImage] collects the transformed endpoints of a one-use -substitution [9, §4.1.4] and gives a [relaxation][singleSubstitutionRelaxation]. The -[**substitution relaxation**][substitutionRelaxation] of a specification is the resources -substituting for a member; it is [compatible with converters][substitutionRelaxation_compatible] -and [idempotent][substitutionRelaxation_idem]. Constructions with simulators -compose [9, Definition 2.4.3 and Theorem 2.4.4]: a witness -[gives serial simulators][Implication.exists_serial_simulators], and -[derivable constructions compose serially][Constructs.derivable_serial_simulators]. - ---- - -## 6. Writing systems: the DSL - -*`interface`, `system`, `converter` and `filter` declarations compile to the typed systems and -typed converters of §2 at every budget ([DSL][DSL], [GRAMMAR][Grammar]); converters are declared -as arrows of the category of interfaces (§3.1), so that components assemble with `≫` and `⊗ₘ`.* A component compiles to a deterministic -[program][Program] and **sources**: every sampling `x ←$ P` [becomes a call][desugarSampling] to -a [source][TypedSystem.source] of fresh samples of the closed law $`P`$, and initialization -runs in the first invocation. - -An [`interface I`][elabInterface] declaration generates `I q := Interface.queryBudget … q`, the -[query budget][Interface.queryBudget], and `I.perPort q := Interface.portBudget … q`, the -[per-port budget][Interface.portBudget]. A [`system S : I`][elabComponent] generates the typed -system `S : TypedSystem (I q)`, [compiled][elabProgramDecls] to `S.program • S.randomness k`: the -[converter of its program][TypedConverter.ofProgram] attached to its [sources][sourcesAt]. A -system that samples nothing is the [automaton][TypedSystem.ofAutomaton] of its program, and -a system without an exact domain [also gets][elabPerPortDecls] -`S.perPort : TypedSystem (I.perPort q)`. - -A [`converter C : I`][elabComponent] with `inside J` generates `C : I q ⟶ J (C.bound * q)`, -compiled to `C.program ≫ TypedConverter.rightContext J (C.randomness k)`: its program with its sources -[beside][TypedConverter.rightContext] the inside interface, or `C.program` when it samples nothing. With -a single inside interface it [also has a per-port typing][elabPerPortDecls] along a partial port -map `C.portMap : I.Port → Option J.Port`, through the -[converter of a port-preserving program][TypedConverter.ofPreservingProgram], with -`C.preserving` a proof of [`Program.PortPreserving`][Program.PortPreserving]. When `J` is `I` and -each procedure calls its own port, at most once, it is -`C.perPort : I.perPort q ⟶ I.perPort q`. When `J` is another interface, each of whose labels one -procedure calls at most once, it is `C.perPort : I.perPort q ⟶ J.perPort (C.insideBudget q)`: an -inside label has the budget of the procedure calling it, and a procedure calling nothing maps to -`none` and needs no inside budget, as in the [write-through cache][WriteThrough] and in -$`\rho^{ctxt}`$ and $`\rho^{ae}`$ of §8. When the converter samples nothing and its number of inside -calls is a function of the input, the elaborator [also generates][elabExactDecls] -`C.exact : (I n).restrict (fun h => (h.map C.cost).sum ≤ q) ⟶ J q`, the -[converter of the costed program][TypedConverter.ofCostedProgram]. - -A [`filter F : I domain h ↦ P`][elabFilter] generates `F : (I q).restrict P ⟶ I q`, the -[filter][TypedConverter.filter] admitting `P`. - -A compiled component is an automaton with a sampled initial state. Attaching a program to an -automaton [gives the combined automaton][TypedConverter.ofProgram_smul_ofAutomaton], also -[for port-preserving programs][TypedConverter.ofPreservingProgram_smul_ofAutomaton], so -compiled systems are compared by [bisimulation][automatonSystem_eq_of_bisim]. The -[memoryless source][MemorylessSource] `y ←$ ν; return y` -[is the memoryless system of `ν`][MemorylessSource.memoryless_eq], so systems built from programs -and memoryless sources are compared by the laws of one reply, through the composition laws of §2.2: -each hop of [PRG length extension][ExPRG] is one rewrite. - ---- - -## 7. Proof commands - -[`cc_normalize`][cc_normalize] rewrites attachments to normal forms, -[`cc_nonexpand`][cc_nonexpand] applies the compatibility laws, on interfaces also -[with the concrete parallel composition][cc_nonexpand-interfaces], [`cc_triangle`][cc_triangle] -takes a hybrid step, and [`cc_construct`][cc_construct] reduces a construction to its equality or -distance obligation. [`cc_calc relation`][cc_calc] proves $`X \simeq Y`$ from `=` and `≃` steps, -and [`cc_calc counted systems`][cc_calc-counted] builds an implication witness, whose uses -[`cc_usage`][cc_usage] counts. [`cc_calc statistical`][cc_calc-statistical] proves -$`d(X, Y) \le \sum_j \varepsilon_j`$ from `≈[ε]` steps, and -[`cc_calc mixed model using domination`][cc_calc-mixed] proves -$`X \simeq_{\sum_j \varepsilon_j} Y`$ from `≃[loss]` and `≈[ε]` steps. - ---- - -## 8. Examples - -- **Authenticated encryption** ([9, Theorem 2.3.10(4)], corrected; [Security][AESec]). Let $`R`$ be - the real system [`AE.Real`][AE.Real], $`E`$ the encryption oracle - [`Encryption.Real`][Encryption.Real], and $`I = \rho^{ae} E`$ the ideal system - (`AE.Ideal • Encryption.Real`): [`AE.Ideal`][AE.Ideal], like [`AE.CTXT`][AE.CTXT] - ($`\rho^{ctxt}`$), is a converter from [`AE M C`][AE] to [`Encryption M C`][Encryption]. Let $`P`$ and $`C`$ be the - [plaintext filter][AE.PTXT] `AE.PTXT` and the [random-message transformation][AE.CCA] `AE.CCA`, - and $`q = (q_e, q_d)`$ the budgets per port. The corrected chain uses each assumption twice: - -```math -R \;\simeq_{\mathrm{ptxt}}\; P R \;\simeq_{\mathrm{cca}}\; P C R \;\simeq_{\mathrm{ptxt}}\; P C P R \;\simeq_{\mathrm{cca}}\; P C P C R \;\approx_{q_e^2 / \lvert \mathcal M \rvert}\; I . -``` - - The last step is the [collision bound][hybrid_ideal_distance_le], which compares the hybrid - with `AE.Ideal.perPort • Encryption.Real.perPort` ([Collision][AECol]). The results are the - [counted witness][correctedChain], with [two uses of ind-cca][correctedChain_cca] and - [two of int-ptxt][correctedChain_ptxt], the [advantage form][ae_of_ind_cca_int_ptxt], and the - [distance form][real_ideal_distance_le] - $`\Delta(R, I) \le 2\,\Delta(R, P R) + 2\,\Delta(R, C R) + q_e^2 / \lvert \mathcal M \rvert`$. - The systems and the notions [`AE.INDCCA`][AE.INDCCA], [`AE.INTPTXT`][AE.INTPTXT], - [`AE.INTCTXT`][AE.INTCTXT] and [`AE.Secure`][AE.Secure] are Commons definitions - ([AEAD][AEDefs]); int-ctxt and ae read $`R \simeq \rho^{ctxt} E`$ and $`R \simeq \rho^{ae} E`$. - The systems are compared as [oracle automata][oracleStep] ([Oracle][AEOracle], - [Hybrid][AEHybrid]), each by a bisimulation of its compiled automaton: the - [real system][real_bisim], the [encryption oracle][encryptionReal_bisim], and the images under - the [plaintext filter][ptxt_bisim], the [random-message transformation][cca_bisim] and the - [ideal transformation][aeIdeal_bisim]. -- **Games** ([Games][ExGames]). In every instance of `Games`: hardness through - [a reduction][win_attach_le], [two reductions][win_attach_comp_le] and - [a lossy reduction][win_le_of_reduction], $`W(G_1) \le k\, W(\alpha \cdot G_2) \le k\, \varepsilon`$, - the shape of a reduction that guesses one of $`k`$ sessions. In every instance of - `DistinctionGames`: a [game hop inside a construction][advantage_attach_le_win], - $`\lvert D(\alpha\, G^-) - D(\alpha T) \rvert \le W(\alpha \cdot G)`$ for $`G \mathrel{|\!\equiv} T`$. - On interfaces, the collision game of authenticated encryption - [is the game the collision discrete game presents][collision], with - [visible typed system the hybrid][collision_visible] and - [conditionally equivalent to the ideal][collision_conditionallyEquivalent]; every winner - [wins it with probability at most][collision_win_le] $`q_e^2 / \lvert \mathcal M \rvert`$, so - every solver's advantage between the hybrid and the ideal - [is at most][hybrid_ideal_advantage_le] $`q_e^2 / \lvert \mathcal M \rvert`$, also - [inside any construction][attach_hybrid_ideal_advantage_le]. -- **Substitutions on interfaces** ([Substitution][ExSub]): single substitutions with a context - [on the right][construction_with_right_context] or [on the left][construction_with_left_context], - and [two statistical substitutions][constructsWithin_of_two_substitutions] giving - $`\lbrace R \rbrace \xrightarrow{\pi,\ \varepsilon_1 + \varepsilon_2} \lbrace \sigma S \rbrace`$. -- **DSL components** ([Components][ExComp]): counters, fresh and persistent randomness, a - [padding converter][Padding] with an inferred cost, the [write-through cache][WriteThrough] - typed by a partial port map, and a [filter][FirstRequests]. -- **AES and AEAD in the DSL** ([AES][ExAES], [AEAD][ExAEAD]): [AES-256][AES-system] as a system - with a random key, from the Commons [block cipher][BlockCipher] [AES][AES-blockCipher], with - converters around it such as [CBC-MAC][CBC]; and [AES-CTR followed by PMAC][EncryptThenMAC], - from the Commons [CTR][CTR] and [PMAC][PMAC] converters. The proof commands on interfaces are - exercised in [Usability][ExUse]. +**Examples.** Authenticated encryption is secure under ind-cca and int-ptxt +[9, Theorem 2.3.10(4)], corrected: a [counted chain][correctedChain] uses each assumption twice, +and a collision bound of $`q_e^2 / \lvert \mathcal M \rvert`$ ends it +([distance form][real_ideal_distance_le]). Games and reductions in every instance of the games +classes, substitutions on interfaces, components, AES and an AEAD in the DSL, and PRG length +extension are in [Examples](src/Examples/README.md). --- @@ -922,43 +263,6 @@ R \;\simeq_{\mathrm{ptxt}}\; P R \;\simeq_{\mathrm{cca}}\; P C R \;\simeq_{\math --- -## Appendix A. Probability - -*Finitely supported laws [1, Definitions 1–4]:* - -```math -\mathrm{Distribution}(A) = A \to_0 \mathbb R, \qquad -\delta(X, Y) = \sum_a \max\big(X(a) - Y(a),\ 0\big) . -``` - -A [**distribution**][Distribution] is a finitely supported function to $`\mathbb R`$, and a -[**probability distribution**][ProbDist] one that is [nonnegative with weight one][isProbDist]. -Distributions have [masses][mass] of events, [pushforwards][fTransform], [products][prod] of two -laws and of [families][pi], and [uniform][uniform] laws. A [**kernel**][bindK] $`f`$ is a conditional -distribution [3, §3.6.1]; mixed over a law $`\mu`$ it gives $`\sum_a \mu(a)\, f(a)`$: -[mixtures compose][bindK_bindK], a pushforward -[is the point kernel of its function][bindK_single_comp], and an independent product -[disintegrates][pi_eq_bindK_update] at a coordinate. Probability laws have -[pushforwards][ProbDist.map] and [sequential compositions][ProbDist.bind]. The -[**statistical distance**][statDist] -satisfies the [triangle inequality][statDist_triangle] and [data processing][statDist_fTransform_le], -$`\delta(fX, fY) \le \delta(X, Y)`$; with [positive parts][statDist_eq_weight_posPart] it is -$`\delta(X, Y) = \lvert (X - Y)^{+} \rvert`$, and with [overlaps][statDist_eq_weight_sub_weight_inf] -$`\delta(X, Y) = \lvert X \rvert - \lvert X \wedge Y \rvert`$. - -For a [coupling][IsCoupling] of $`X`$ and $`Y`$, -[the distance is at most the off-diagonal mass][statDist_le_offDiagonalMass], -$`\delta(X, Y) \le \Pr[X \ne Y]`$, and [some coupling attains it][exists_coupling_offDiagonalMass_eq]. -For the $`n`$-ary maximal coupling [2, Theorem 2.29], the [largest agreement][supAgreement] of $`n`$ -laws of one weight [is the weight of their overlap][supAgreement_eq_weight_overlapDist]. -[**Expectation**][expect] is linear [in the distribution][expect_add_left] and -[in the function][expect_add_right], with [Markov's][mass_ge_le_expect_div], -the [Cauchy–Schwarz][expect_mul_sq_le_sq_mul_sq] and [Jensen's][ConvexOn.map_expect_le] -inequalities. Collision bounds [count][card_function_fiber_finset] the functions $`X \to Y`$ -agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X \rvert - \lvert S \rvert}`$. - ---- - ## References 1. D. Lanzenberger and U. Maurer. Coupling of Random Systems. In *Theory of Cryptography (TCC 2020)*, Springer, 2020. Cryptology ePrint Archive, Paper 2020/1187. @@ -976,57 +280,23 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X [DSL]: src/ConstructiveCryptography/DSL.lean [Grammar]: src/ConstructiveCryptography/DSL/GRAMMAR.md [SymEnc]: src/Commons/Definitions/Encryption.lean -[AEDefs]: src/Commons/Definitions/AEAD.lean -[AEOracle]: src/Examples/AuthenticatedEncryption/Oracle.lean -[AEHybrid]: src/Examples/AuthenticatedEncryption/Hybrid.lean [AECol]: src/Examples/AuthenticatedEncryption/Collision.lean [AESec]: src/Examples/AuthenticatedEncryption/Security.lean -[ExSub]: src/Examples/Substitution.lean -[ExGames]: src/Examples/Games.lean -[ExComp]: src/Examples/DSL/Components.lean -[ExAES]: src/Examples/DSL/AES.lean -[ExAEAD]: src/Examples/DSL/AEAD.lean -[ExUse]: src/Examples/Usability.lean -[ExPRG]: src/Examples/PRGLengthExtension.lean -[System]: src/RandomSystems/System/Basic.lean#L40 -[SilentAtEmpty]: src/RandomSystems/System/Basic.lean#L69 -[PrefixClosed]: src/RandomSystems/System/Basic.lean#L72 [IsDDS]: src/RandomSystems/System/Basic.lean#L77 -[interconnect]: src/RandomSystems/System/Basic.lean#L225 -[restrict]: src/RandomSystems/System/Basic.lean#L794 -[Replies]: src/RandomSystems/System/Replies.lean#L33 -[IsDDS.eq_of_replies_iff]: src/RandomSystems/System/Replies.lean#L151 -[automatonSystem]: src/RandomSystems/System/Automaton.lean#L43 -[IsBisim]: src/RandomSystems/System/Automaton.lean#L70 [automatonSystem_eq_of_bisim]: src/RandomSystems/System/Automaton.lean#L89 -[DDE]: src/RandomSystems/System/DDE.lean#L20 -[QueryBounded]: src/RandomSystems/System/DDE.lean#L24 [Domain]: src/RandomSystems/PDS/PDS.lean#L65 -[Equivalent]: src/RandomSystems/PDS/PDS.lean#L50 -[HasDomain]: src/RandomSystems/PDS/PDS.lean#L91 [PDS]: src/RandomSystems/PDS/PDS.lean#L133 [IsRandomSystem]: src/RandomSystems/Cumulative/Cumulative.lean#L39 [RandomSystem]: src/RandomSystems/Cumulative/Cumulative.lean#L53 [RandomSystem.RepliesAtQueriedInterface]: src/RandomSystems/Cumulative/Cumulative.lean#L70 [PDS.behavior]: src/RandomSystems/Cumulative/Cumulative.lean#L216 -[PDS.behavior_eq_iff]: src/RandomSystems/Cumulative/Cumulative.lean#L225 [RandomSystem.exists_presentation]: src/RandomSystems/Cumulative/Presentation.lean#L302 [RandomSystem.ofPDSClass_bijective]: src/RandomSystems/Cumulative/Presentation.lean#L312 -[RandomSystem.sLaw]: src/RandomSystems/Cumulative/CumulativeObservation.lean#L179 -[RandomSystem.Compatible]: src/RandomSystems/Cumulative/CumulativeObservation.lean#L197 -[RandomSystem.eq_iff_sLaw]: src/RandomSystems/Cumulative/CumulativeObservation.lean#L534 -[RandomSystem.eq_iff_sLaw_fixedQueries]: src/RandomSystems/Cumulative/CumulativeObservation.lean#L548 -[RandomSystem.mix]: src/RandomSystems/Cumulative/CumulativeOperations.lean#L45 [RandomSystem.parallel]: src/RandomSystems/Cumulative/CumulativeOperations.lean#L130 [IsDDC]: src/RandomSystems/DDC/DDC.lean#L127 -[serialM]: src/RandomSystems/DDC/Serial.lean#L55 -[IsDDC.comp]: src/RandomSystems/DDC/Serial.lean#L514 -[converterDomain]: src/RandomSystems/Converter/ConverterDomain.lean#L234 -[IsDDCFrom]: src/RandomSystems/Converter/ConverterDomain.lean#L301 -[IsDDCFrom.mapsDomain]: src/RandomSystems/Converter/ConverterDomain.lean#L609 [PDCBehavior]: src/RandomSystems/Converter/PDCBehavior.lean#L67 [PDCBehavior.ofPDC]: src/RandomSystems/Converter/PDCBehavior.lean#L169 [PDCBehavior.comp]: src/RandomSystems/Converter/PDCBehavior.lean#L273 @@ -1035,174 +305,75 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X [PDCBehavior.id_comp]: src/RandomSystems/Converter/PDCBehavior.lean#L385 [PDCBehavior.comp_id]: src/RandomSystems/Converter/PDCBehavior.lean#L375 [PDCBehavior.attach]: src/RandomSystems/Converter/ConverterAttachment.lean#L156 -[PDCBehavior.attach_presents]: src/RandomSystems/Converter/ConverterAttachment.lean#L178 [PDCBehavior.attach_id]: src/RandomSystems/Converter/ConverterAttachment.lean#L233 [PDCBehavior.attach_comp]: src/RandomSystems/Converter/ConverterAttachment.lean#L246 [PDCBehavior.tensor]: src/RandomSystems/Converter/ConverterTensor.lean#L649 [PDCBehavior.comp_tensor]: src/RandomSystems/Converter/ConverterTensor.lean#L745 [PDCBehavior.tensor_id]: src/RandomSystems/Converter/ConverterTensor.lean#L705 [Program]: src/RandomSystems/Converter/Program.lean#L45 -[Program.Bounded]: src/RandomSystems/Converter/Program.lean#L70 -[Program.Costs]: src/RandomSystems/Converter/Program.lean#L112 -[Program.PortPreserving]: src/RandomSystems/Converter/Program.lean#L123 -[DDC.insideQueries_restrict_length_le]: src/RandomSystems/Converter/Program.lean#L537 -[DDC.ofProgramOn_isDDCFrom]: src/RandomSystems/Converter/Program.lean#L634 -[Program.inline]: src/RandomSystems/Converter/ProgramAttachment.lean#L258 -[Program.combine]: src/RandomSystems/Converter/ProgramAttachment.lean#L429 -[Program.trim_apply_ofProgramOn_automaton]: src/RandomSystems/Converter/ProgramAttachment.lean#L609 -[RandomSystem.ofProbAutomaton]: src/RandomSystems/System/ProbAutomaton.lean#L197 -[ProbStep]: src/RandomSystems/System/ProbAutomaton.lean#L58 -[ProbStep.belief]: src/RandomSystems/System/ProbAutomaton.lean#L160 -[ProbStep.SimulatesAt]: src/RandomSystems/System/ProbAutomaton.lean#L260 -[RandomSystem.ofProbAutomaton_eq_of_simulation]: src/RandomSystems/System/ProbAutomaton.lean#L400 -[RandomSystem.ofProbAutomaton_ofDeterministic_apply]: src/RandomSystems/System/ProbAutomaton.lean#L535 -[RandomSystem.ofProbAutomaton_eq_drawStep]: src/RandomSystems/Converter/ProbProgramAttachment.lean#L933 -[RandomSystem.memoryless]: src/RandomSystems/System/Memoryless.lean#L65 -[RandomSystem.eq_memoryless_of_snoc]: src/RandomSystems/System/Memoryless.lean#L84 -[RandomSystem.parallel_memoryless]: src/RandomSystems/System/Memoryless.lean#L146 -[ProbStep.Memoryless]: src/RandomSystems/System/Memoryless.lean#L237 -[RandomSystem.ofProbAutomaton_eq_memoryless]: src/RandomSystems/System/Memoryless.lean#L273 -[Program.probCombine]: src/RandomSystems/Converter/ProbProgramAttachment.lean#L187 -[RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation]: src/RandomSystems/Converter/ProbProgramAttachment.lean#L507 -[PDCBehavior.attach_ofDDC_ofProgramOn_ofProbAutomaton]: src/RandomSystems/Converter/ProbProgramAttachment.lean#L1095 -[PDCBehavior.attach_ofDDC_ofProgramOn_ofDeterministic]: src/RandomSystems/Converter/ProbProgramAttachment.lean#L1009 -[Program.memoryless_probCombine]: src/RandomSystems/System/Memoryless.lean#L390 -[Program.replyLaw]: src/RandomSystems/System/Memoryless.lean#L304 -[PDCBehavior.attach_ofDDC_ofProgramOn_memoryless]: src/RandomSystems/System/Memoryless.lean#L421 [RandomSystem.transcriptDistance]: src/RandomSystems/Distance/Decision.lean#L228 -[Domain.Compatible]: src/RandomSystems/Distance/Decision.lean#L165 -[Domain.DecisionCompatible]: src/RandomSystems/Distance/Decision.lean#L171 -[IsDDD]: src/RandomSystems/System/InterfaceSystem.lean#L968 -[RandomSystem.decisionProbability]: src/RandomSystems/Distance/Decision.lean#L262 [Domain.Distinguisher]: src/RandomSystems/Distance/Distinguisher.lean#L122 -[Domain.Distinguisher.probability]: src/RandomSystems/Distance/Distinguisher.lean#L126 -[Domain.Distinguisher.advantage]: src/RandomSystems/Distance/Distinguisher.lean#L132 -[advantage_self]: src/RandomSystems/Distance/Distinguisher.lean#L141 -[advantage_symm]: src/RandomSystems/Distance/Distinguisher.lean#L143 -[advantage_triangle]: src/RandomSystems/Distance/Distinguisher.lean#L146 [RandomSystem.transcriptDistance_eq_iSup]: src/RandomSystems/Distance/Distinguisher.lean#L154 -[advantage_le_transcriptDistance]: src/RandomSystems/Distance/Distinguisher.lean#L196 [Domain.DistinguisherBehavior]: src/RandomSystems/Distance/Distinguisher.lean#L207 -[DistinguisherBehavior.advantage]: src/RandomSystems/Distance/Distinguisher.lean#L218 -[DistinguisherBehavior.advantage_self]: src/RandomSystems/Distance/Distinguisher.lean#L228 -[DistinguisherBehavior.advantage_symm]: src/RandomSystems/Distance/Distinguisher.lean#L230 -[DistinguisherBehavior.advantage_triangle]: src/RandomSystems/Distance/Distinguisher.lean#L233 -[DistinguisherBehavior.advantage_le_transcriptDistance]: src/RandomSystems/Distance/Distinguisher.lean#L238 -[RandomSystem.transcriptDistance_eq_iSup_behavior]: src/RandomSystems/Distance/Distinguisher.lean#L246 -[System.tr]: src/RandomSystems/Distance/Coupling.lean#L50 -[PDS.sLaw_behavior_eq_fTransform]: src/RandomSystems/Distance/Coupling.lean#L165 -[PDS.statDist_sLaw_behavior_le_of_isCoupling]: src/RandomSystems/Distance/Coupling.lean#L213 -[PDS.transcriptDistance_behavior_le_of_isCoupling]: src/RandomSystems/Distance/Coupling.lean#L241 [DistinguisherBehavior.absorb]: src/RandomSystems/Distance/Distinguisher.lean#L291 -[DistinguisherBehavior.absorb_comp]: src/RandomSystems/Distance/Distinguisher.lean#L304 -[Domain.Distinguisher.exists_absorbAll]: src/RandomSystems/Distance/Distinguisher.lean#L265 [Domain.Distinguisher.exists_absorbRight]: src/RandomSystems/Distance/Distinguisher.lean#L330 -[absorbAll]: src/RandomSystems/Distance/Absorption.lean#L42 -[RandomSystem.restrict]: src/RandomSystems/Distance/Restriction.lean#L59 -[RandomSystem.restrict_restrict]: src/RandomSystems/Distance/Restriction.lean#L67 -[RandomSystem.sLaw_restrict]: src/RandomSystems/Distance/Restriction.lean#L98 -[RandomSystem.transcriptDistance_restrict_le]: src/RandomSystems/Distance/Restriction.lean#L129 -[RandomSystem.transcriptDistance_le_add_of_ratio_on_good]: src/RandomSystems/Distance/HCoefficient.lean#L40 -[MC]: src/RandomSystems/Game/DiscreteMBO.lean#L46 -[DDG]: src/RandomSystems/Game/DiscreteMBO.lean#L50 -[PDG]: src/RandomSystems/Game/DiscreteMBO.lean#L54 -[PDG.ofFunction]: src/RandomSystems/Game/FunctionGame.lean#L37 [RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L305 [RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L340 -[DDE.blindMBO]: src/RandomSystems/Game/MBO.lean#L410 [RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L480 [RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L523 -[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L756 -[Domain.Distinguisher.winProbability_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L951 -[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L976 [RandomSystem.GameEquivalent]: src/RandomSystems/Game/MBO.lean#L537 -[Domain.Distinguisher.winProbability_eq_of_gameEquivalent]: src/RandomSystems/Game/MBO.lean#L860 +[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L756 [Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent]: src/RandomSystems/Game/MBO.lean#L874 -[transcriptCost]: src/RandomSystems/Distance/UntilBad.lean#L38 -[RandomSystem.one_sub_le_sum_tSupp]: src/RandomSystems/Distance/UntilBad.lean#L65 -[RandomSystem.transcriptDistance_le_of_transcriptCost_le]: src/RandomSystems/Distance/UntilBad.lean#L146 -[Domain.Distinguisher.winProbability_le_of_transcriptCost_le]: src/RandomSystems/Game/UntilBad.lean#L148 -[RandomSystem.GameEquivalent.transcriptDistance_visible_le]: src/RandomSystems/Game/UntilBad.lean#L177 -[PDG.gameEquivalent_behavior_of_isCoupling]: src/RandomSystems/Game/UntilBad.lean#L209 [PDCBehavior.liftMBO]: src/RandomSystems/Game/MBOAttachment.lean#L455 [PDCBehavior.liftMBO_id]: src/RandomSystems/Game/MBOAttachment.lean#L495 [PDCBehavior.liftMBO_comp]: src/RandomSystems/Game/MBOAttachment.lean#L1515 -[RandomSystem.MonotoneMBO.attach_liftMBO]: src/RandomSystems/Game/MBOAttachment.lean#L965 [RandomSystem.visible_attach_liftMBO]: src/RandomSystems/Game/MBOAttachment.lean#L619 -[RandomSystem.winProbability_attach_liftMBO]: src/RandomSystems/Game/MBOAttachment.lean#L2079 [Domain.SolverBehavior]: src/RandomSystems/Game/MBOAttachment.lean#L2169 [Domain.SolverBehavior.absorb]: src/RandomSystems/Game/MBOAttachment.lean#L2191 -[DDG.withMBO]: src/RandomSystems/Game/DiscreteMBO.lean#L103 -[PDG.behavior]: src/RandomSystems/Game/DiscreteMBO.lean#L235 -[PDG.visible_behavior]: src/RandomSystems/Game/DiscreteMBO.lean#L253 -[PDG.unsetProbability_behavior]: src/RandomSystems/Game/DiscreteMBO.lean#L331 -[PDG.one_sub_le_unsetProbability_behavior]: src/RandomSystems/Game/DiscreteMBO.lean#L434 -[PDG.conditionallyEquivalent_behavior]: src/RandomSystems/Game/DiscreteMBO.lean#L460 -[PDG.ofFunction_conditionallyEquivalent]: src/RandomSystems/Game/FunctionGame.lean#L73 [Interface]: src/RandomSystems/Typed/Interface.lean#L40 -[Interface.queryBudget]: src/RandomSystems/Typed/Interface.lean#L63 -[Interface.portBudget]: src/RandomSystems/Typed/Interface.lean#L74 [TypedSystem]: src/RandomSystems/Typed/Interface.lean#L92 [TypedConverter]: src/RandomSystems/Typed/Interface.lean#L127 -[Interface.category]: src/ConstructiveCryptography/InterfaceCategory.lean#L30 -[TypedConverter.ofDDC]: src/RandomSystems/Typed/Interface.lean#L143 -[TypedConverter.attach]: src/RandomSystems/Typed/Interface.lean#L157 [TypedConverter.comp]: src/RandomSystems/Typed/Interface.lean#L134 [TypedConverter.id]: src/RandomSystems/Typed/Interface.lean#L139 +[TypedConverter.attach]: src/RandomSystems/Typed/Interface.lean#L157 [TypedConverter.identity_attach]: src/RandomSystems/Typed/Interface.lean#L171 [TypedConverter.comp_smul]: src/RandomSystems/Typed/Interface.lean#L177 -[Interface.identity_attach]: src/ConstructiveCryptography/InterfaceCategory.lean#L45 -[Interface.comp_smul]: src/ConstructiveCryptography/InterfaceCategory.lean#L50 [Interface.tensor]: src/RandomSystems/Typed/Parallel.lean#L85 [TypedSystem.parallel]: src/RandomSystems/Typed/Parallel.lean#L153 [TypedConverter.parallel]: src/RandomSystems/Typed/Parallel.lean#L210 -[Interface.restrict]: src/RandomSystems/Typed/Filter.lean#L32 -[TypedConverter.filter]: src/RandomSystems/Typed/Filter.lean#L49 -[TypedConverter.filter_smul]: src/RandomSystems/Typed/Filter.lean#L60 -[TypedConverter.filter_comp_filter_smul]: src/RandomSystems/Typed/Filter.lean#L94 -[TypedConverter.constant]: src/RandomSystems/Typed/Context.lean#L78 -[TypedConverter.rightContext]: src/RandomSystems/Typed/Context.lean#L109 -[TypedConverter.leftContext]: src/RandomSystems/Typed/Context.lean#L116 -[TypedConverter.attach_rightContext]: src/RandomSystems/Typed/Context.lean#L122 -[TypedConverter.attach_leftContext]: src/RandomSystems/Typed/Context.lean#L127 +[TypedConverter.parallel_attach]: src/RandomSystems/Typed/ParallelAttachment.lean#L23 +[Interface.unit]: src/RandomSystems/Typed/InterfaceCoherence.lean#L90 +[TypedConverter.rename]: src/RandomSystems/Typed/Relabel.lean#L48 +[TypedConverter.rename_comp]: src/RandomSystems/Typed/Relabel.lean#L80 +[TypedConverter.rename_refl]: src/RandomSystems/Typed/Relabel.lean#L67 +[TypedConverter.rename_mass]: src/RandomSystems/Typed/SystemParallel.lean#L55 +[TypedConverter.comp_associator]: src/RandomSystems/Typed/ConverterCoherence.lean#L158 +[TypedConverter.comp_leftUnitor]: src/RandomSystems/Typed/ConverterCoherence.lean#L195 +[TypedConverter.comp_rightUnitor]: src/RandomSystems/Typed/ConverterCoherence.lean#L224 +[TypedConverter.parallel_rename]: src/RandomSystems/Typed/TensorRename.lean#L128 +[TypedSystem.dummy]: src/RandomSystems/Typed/SystemCoherence.lean#L97 +[TypedSystem.parallel_assoc_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L85 +[TypedSystem.parallel_unit_left_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L103 +[TypedSystem.parallel_unit_right_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L128 +[TypedSystem.parallel_swap_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L153 [TypedSystem.source]: src/RandomSystems/Typed/Source.lean#L51 -[TypedSystem.ofAutomaton]: src/RandomSystems/Typed/Automaton.lean#L42 -[TypedSystem.parallel_ofAutomaton]: src/RandomSystems/Typed/Automaton.lean#L57 -[TypedSystem.source_eq_memoryless]: src/RandomSystems/Typed/Memoryless.lean#L47 -[TypedSystem.parallel_eq_memoryless]: src/RandomSystems/Typed/Memoryless.lean#L146 -[TypedConverter.ofProgram_smul_memoryless]: src/RandomSystems/Typed/Memoryless.lean#L241 -[TypedConverter.ofPreservingProgram_smul_memoryless]: src/RandomSystems/Typed/Memoryless.lean#L262 -[TypedConverter.ofPreservingProgram_comp_rightContext_smul_memoryless]: src/RandomSystems/Typed/Memoryless.lean#L279 -[TypedSystem.ofFunction]: src/RandomSystems/Typed/Functional.lean#L56 -[TypedSystem.ofConditional]: src/RandomSystems/Typed/Functional.lean#L38 -[TypedSystem.sample]: src/RandomSystems/Typed/Functional.lean#L176 -[Interface.withMBO]: src/RandomSystems/Typed/Game.lean#L24 [TypedGame]: src/RandomSystems/Typed/Game.lean#L35 [TypedConverter.attachGame]: src/RandomSystems/Typed/Game.lean#L38 [TypedGame.visible]: src/RandomSystems/Typed/Game.lean#L53 -[TypedGame.ofPDG]: src/RandomSystems/Typed/PresentedGame.lean#L41 -[TypedGame.visible_ofPDG]: src/RandomSystems/Typed/PresentedGame.lean#L51 -[Interface.conditionallyEquivalent_ofPDG_iff]: src/ConstructiveCryptography/InterfaceGame.lean#L200 -[Interface.game_dist_le]: src/ConstructiveCryptography/InterfaceGame.lean#L213 -[TypedGame.ofSingleFunction]: src/RandomSystems/Typed/PresentedGame.lean#L88 -[TypedGame.ofSingleFunction_conditionallyEquivalent]: src/RandomSystems/Typed/PresentedGame.lean#L101 -[Interface.swap]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L66 -[Interface.parallel_swap]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L107 -[notation-distance]: src/ConstructiveCryptography/Notation.lean#L24 -[notation-parallel]: src/ConstructiveCryptography/Notation.lean#L28 -[notation-constructs]: src/ConstructiveCryptography/Notation.lean#L31 -[notation-constructsWithin]: src/ConstructiveCryptography/Notation.lean#L35 -[notation-substitutes]: src/ConstructiveCryptography/Notation.lean#L41 -[notation-conditionallyEquivalent]: src/ConstructiveCryptography/Notation.lean#L47 +[Interface.category]: src/ConstructiveCryptography/InterfaceCategory.lean#L30 [Interface.monoidalStruct]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L71 [Interface.monoidal]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L162 [Interface.isoOf]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L33 +[Interface.associator]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L52 +[Interface.leftUnitor]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L57 +[Interface.rightUnitor]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L61 +[Interface.swap]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L66 [Interface.id_tensor_id]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L84 [Interface.tensor_comp]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L87 [Interface.associator_naturality]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L92 @@ -1210,28 +381,19 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X [Interface.rightUnitor_naturality]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L101 [Interface.pentagon]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L105 [Interface.triangle]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L132 -[Interface.unit]: src/RandomSystems/Typed/InterfaceCoherence.lean#L90 -[Interface.associator]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L52 -[Interface.leftUnitor]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L57 -[Interface.rightUnitor]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L61 -[TypedConverter.comp_associator]: src/RandomSystems/Typed/ConverterCoherence.lean#L158 -[TypedConverter.comp_leftUnitor]: src/RandomSystems/Typed/ConverterCoherence.lean#L195 -[TypedConverter.comp_rightUnitor]: src/RandomSystems/Typed/ConverterCoherence.lean#L224 -[TypedConverter.parallel_rename]: src/RandomSystems/Typed/TensorRename.lean#L128 -[TypedConverter.rename]: src/RandomSystems/Typed/Relabel.lean#L48 -[TypedConverter.rename_comp]: src/RandomSystems/Typed/Relabel.lean#L80 -[TypedConverter.rename_refl]: src/RandomSystems/Typed/Relabel.lean#L67 -[TypedConverter.rename_mass]: src/RandomSystems/Typed/SystemParallel.lean#L55 [ResourceTheory]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L50 -[ResourceTheory.functor]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L69 [CryptographicAlgebra]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L97 -[CA.parallel]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L126 -[CA.dummy]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L134 -[CA.attach_parallel]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L160 -[CA.parallel_assoc]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L182 -[CA.parallel_dummy_left]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L196 -[CA.parallel_dummy_right]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L211 +[CompatiblePseudoMetric]: src/ConstructiveCryptography/CryptographicAlgebra/PseudoMetric.lean#L43 +[advantageDistance]: src/ConstructiveCryptography/CryptographicAlgebra/Distinguisher.lean#L36 +[CompatibleDistinguisherClass]: src/ConstructiveCryptography/CryptographicAlgebra/Distinguisher.lean#L77 +[CompatibleDistinguisherClass.ofClosure]: src/ConstructiveCryptography/CryptographicAlgebra/Distinguisher.lean#L102 +[Games]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L62 +[DistinctionGames]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L112 [Interface.resourceTheory]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L71 +[Interface.parallel_assoc]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L77 +[Interface.parallel_dummy_left]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L89 +[Interface.parallel_dummy_right]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L98 +[Interface.parallel_swap]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L107 [Interface.resourcesLaxMonoidal]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L116 [Interface.cryptographicAlgebra]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L142 [Interface.distinguishers]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L148 @@ -1242,210 +404,36 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X [Interface.cc_parallel_eq]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L188 [Interface.cc_dummy_eq]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L192 [Interface.cc_distance_eq]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L196 -[TypedSystem.dummy]: src/RandomSystems/Typed/SystemCoherence.lean#L97 -[TypedSystem.parallel_assoc_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L85 -[TypedSystem.parallel_unit_left_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L103 -[TypedSystem.parallel_unit_right_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L128 -[TypedSystem.parallel_swap_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L153 -[Interface.parallel_assoc]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L77 -[Interface.parallel_dummy_left]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L89 -[Interface.parallel_dummy_right]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L98 -[TypedConverter.parallel_attach]: src/RandomSystems/Typed/ParallelAttachment.lean#L23 -[CompatiblePseudoMetric]: src/ConstructiveCryptography/CryptographicAlgebra/PseudoMetric.lean#L43 -[CA.distance]: src/ConstructiveCryptography/CryptographicAlgebra/PseudoMetric.lean#L63 -[distance_attach_le]: src/ConstructiveCryptography/CryptographicAlgebra/PseudoMetric.lean#L90 -[distance_parallel_le]: src/ConstructiveCryptography/CryptographicAlgebra/PseudoMetric.lean#L145 -[advantageDistance]: src/ConstructiveCryptography/CryptographicAlgebra/Distinguisher.lean#L36 -[CompatibleDistinguisherClass]: src/ConstructiveCryptography/CryptographicAlgebra/Distinguisher.lean#L77 -[CompatibleDistinguisherClass.ofClosure]: src/ConstructiveCryptography/CryptographicAlgebra/Distinguisher.lean#L102 - -[Games]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L62 -[DistinctionGames]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L112 -[Games.absorb]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L93 -[DistinctionGames.absorb]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L148 -[Games.absorb_comp]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L101 +[Interface.winners]: src/ConstructiveCryptography/InterfaceGame.lean#L58 +[Interface.solvers]: src/ConstructiveCryptography/InterfaceGame.lean#L63 [Interface.games]: src/ConstructiveCryptography/InterfaceGame.lean#L69 [Interface.distinctionGames]: src/ConstructiveCryptography/InterfaceGame.lean#L125 [Interface.dist_visible_le]: src/ConstructiveCryptography/InterfaceGame.lean#L186 -[Interface.winners]: src/ConstructiveCryptography/InterfaceGame.lean#L58 -[Interface.solvers]: src/ConstructiveCryptography/InterfaceGame.lean#L63 -[Interface.win_le]: src/ConstructiveCryptography/InterfaceGame.lean#L170 [Specification]: src/ConstructiveCryptography/Specification/Defs.lean#L18 -[Specification.Constructs]: src/ConstructiveCryptography/Specification/Basic.lean#L31 -[Specification.ConstructsWithin]: src/ConstructiveCryptography/Specification/Metric.lean#L23 -[CA.Specification.Constructs]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L368 -[CA.Specification.ConstructsWithin]: src/ConstructiveCryptography/CryptographicAlgebra/PseudoMetric.lean#L179 -[Constructs.serial]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L443 -[ConstructsWithin.serial]: src/ConstructiveCryptography/CryptographicAlgebra/PseudoMetric.lean#L234 -[Constructs.parallel]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L518 -[ConstructsWithin.parallel]: src/ConstructiveCryptography/CryptographicAlgebra/PseudoMetric.lean#L254 [Relaxation]: src/ConstructiveCryptography/Specification/Relaxation/Defs.lean#L22 -[Relaxation.Compatible]: src/ConstructiveCryptography/CryptographicAlgebra/Relaxation.lean#L46 -[Relaxation.compatible_iff]: src/ConstructiveCryptography/CryptographicAlgebra/Relaxation.lean#L84 -[Constructs.relax_serial]: src/ConstructiveCryptography/CryptographicAlgebra/Relaxation.lean#L136 -[epsilonRelaxation]: src/ConstructiveCryptography/CryptographicAlgebra/Epsilon.lean#L43 -[constructs_epsilonRelaxation_iff]: src/ConstructiveCryptography/CryptographicAlgebra/Epsilon.lean#L165 -[Constructs.serial_epsilonRelaxation]: src/ConstructiveCryptography/CryptographicAlgebra/Epsilon.lean#L225 -[CA.star]: src/ConstructiveCryptography/CryptographicAlgebra/Star.lean#L59 -[star_idem]: src/ConstructiveCryptography/CryptographicAlgebra/Star.lean#L94 -[starClosure]: src/ConstructiveCryptography/Specification/Star.lean#L55 -[Constructs.star]: src/ConstructiveCryptography/CryptographicAlgebra/Star.lean#L145 [constructs_of_simulator]: src/ConstructiveCryptography/CryptographicAlgebra/Star.lean#L269 -[kernel]: src/ConstructiveCryptography/Specification/Relaxation/Kernel.lean#L16 -[gameSpec]: src/ConstructiveCryptography/Specification/Game/Basic.lean#L24 -[Constructible]: src/ConstructiveCryptography/Construction/Defs.lean#L24 - - - -[SubstitutionRelation]: src/ConstructiveCryptography/Substitution/Basic.lean#L45 +[ConstructsWithin.serial]: src/ConstructiveCryptography/CryptographicAlgebra/PseudoMetric.lean#L234 +[ConstructsWithin.parallel]: src/ConstructiveCryptography/CryptographicAlgebra/PseudoMetric.lean#L254 [Implication]: src/ConstructiveCryptography/Substitution/Basic.lean#L176 -[Implication.usageCount]: src/ConstructiveCryptography/Substitution/Basic.lean#L207 -[substitutes_of_hybrid]: src/ConstructiveCryptography/Substitution/Basic.lean#L77 -[distance_hybrid_le]: src/ConstructiveCryptography/Substitution/Basic.lean#L120 -[Implication.substitutes]: src/ConstructiveCryptography/Substitution/Basic.lean#L214 -[Implication.distance_le]: src/ConstructiveCryptography/Substitution/Basic.lean#L254 -[Implication.map]: src/ConstructiveCryptography/Substitution/Implication.lean#L127 -[Implication.reverse]: src/ConstructiveCryptography/Substitution/Implication.lean#L158 -[Implication.append]: src/ConstructiveCryptography/Substitution/Implication.lean#L207 -[usageCount_append]: src/ConstructiveCryptography/Substitution/Implication.lean#L275 -[generatedRelation]: src/ConstructiveCryptography/Substitution/Implication.lean#L309 -[derivable_substitutes]: src/ConstructiveCryptography/Substitution/Implication.lean#L335 -[DistinguisherAdvantage]: src/ConstructiveCryptography/Substitution/Reduction.lean#L46 [SubstitutesWithin]: src/ConstructiveCryptography/Substitution/Reduction.lean#L72 -[SubstitutesWithin.symm]: src/ConstructiveCryptography/Substitution/Reduction.lean#L80 -[SubstitutesWithin.trans]: src/ConstructiveCryptography/Substitution/Reduction.lean#L94 -[SubstitutesWithin.of_distance]: src/ConstructiveCryptography/Substitution/Reduction.lean#L127 -[SubstitutesWithin.of_statistical]: src/ConstructiveCryptography/Substitution/Reduction.lean#L110 -[SubstitutesWithin.attach]: src/ConstructiveCryptography/Substitution/Reduction.lean#L145 -[SubstitutesWithin.attach_serial]: src/ConstructiveCryptography/Substitution/Reduction.lean#L175 [Implication.substitutesWithin]: src/ConstructiveCryptography/Substitution/Quantitative.lean#L49 [Implication.substitutesWithin_of_mixed]: src/ConstructiveCryptography/Substitution/Quantitative.lean#L105 [Interface.distinguisherAdvantage]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L208 -[Interface.distinguisherAdvantage_attach]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L220 -[Interface.distinguisherAdvantage_le_distance]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L280 -[Interface.substitutesWithin_attach]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L231 -[Interface.AdmissibleDistinguishers]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L246 -[AdmissibleDistinguishers.substitutesWithin_attach]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L255 -[substitutionImage]: src/ConstructiveCryptography/Substitution/Relaxation.lean#L45 -[singleSubstitutionRelaxation]: src/ConstructiveCryptography/Substitution/Relaxation.lean#L59 -[substitutionRelaxation]: src/ConstructiveCryptography/Substitution/Relaxation.lean#L164 -[substitutionRelaxation_compatible]: src/ConstructiveCryptography/Substitution/Relaxation.lean#L182 -[substitutionRelaxation_idem]: src/ConstructiveCryptography/Substitution/Relaxation.lean#L202 -[Implication.exists_serial_simulators]: src/ConstructiveCryptography/Substitution/Construction.lean#L44 -[Constructs.derivable_serial_simulators]: src/ConstructiveCryptography/Substitution/Construction.lean#L107 - + -[desugarSampling]: src/ConstructiveCryptography/DSL/Elaborator.lean#L194 -[elabInterface]: src/ConstructiveCryptography/DSL/Elaborator.lean#L351 -[elabComponent]: src/ConstructiveCryptography/DSL/Elaborator.lean#L811 -[elabProgramDecls]: src/ConstructiveCryptography/DSL/Elaborator.lean#L644 -[elabPerPortDecls]: src/ConstructiveCryptography/DSL/Elaborator.lean#L541 -[elabExactDecls]: src/ConstructiveCryptography/DSL/Elaborator.lean#L716 -[elabFilter]: src/ConstructiveCryptography/DSL/Elaborator.lean#L927 -[sourcesAt]: src/ConstructiveCryptography/DSL/Elaborator.lean#L635 -[TypedConverter.ofProgram]: src/RandomSystems/Typed/DSL/Converters.lean#L39 -[TypedConverter.ofCostedProgram]: src/RandomSystems/Typed/DSL/Converters.lean#L51 -[TypedConverter.ofPreservingProgram]: src/RandomSystems/Typed/DSL/Converters.lean#L68 -[TypedConverter.ofProgram_smul_ofAutomaton]: src/RandomSystems/Typed/DSL/Converters.lean#L145 -[TypedConverter.ofPreservingProgram_smul_ofAutomaton]: src/RandomSystems/Typed/DSL/Converters.lean#L155 -[MemorylessSource]: src/Commons/Definitions/Ideal.lean#L95 -[MemorylessSource.memoryless_eq]: src/Commons/Definitions/Ideal.lean#L103 [cc_normalize]: src/ConstructiveCryptography/Tactics/Basic.lean#L30 [cc_nonexpand]: src/ConstructiveCryptography/Tactics/Categorical.lean#L166 -[cc_nonexpand-interfaces]: src/ConstructiveCryptography/Notation.lean#L105 [cc_triangle]: src/ConstructiveCryptography/Tactics/Categorical.lean#L155 [cc_construct]: src/ConstructiveCryptography/Tactics/Categorical.lean#L42 [cc_calc]: src/ConstructiveCryptography/Tactics/Substitution.lean#L88 -[cc_calc-counted]: src/ConstructiveCryptography/Tactics/Substitution.lean#L147 -[cc_usage]: src/ConstructiveCryptography/Tactics/Substitution.lean#L243 -[cc_calc-statistical]: src/ConstructiveCryptography/Tactics/Substitution.lean#L292 -[cc_calc-mixed]: src/ConstructiveCryptography/Tactics/Substitution.lean#L295 - - - -[AE.Real]: src/Commons/Definitions/AEAD.lean#L54 -[AE]: src/Commons/Definitions/AEAD.lean#L37 -[Encryption]: src/Commons/Definitions/Encryption.lean#L54 -[AE.CCA]: src/Commons/Definitions/AEAD.lean#L65 -[AE.PTXT]: src/Commons/Definitions/AEAD.lean#L84 -[AE.CTXT]: src/Commons/Definitions/AEAD.lean#L98 -[AE.Ideal]: src/Commons/Definitions/AEAD.lean#L111 -[AE.INDCCA]: src/Commons/Definitions/AEAD.lean#L165 -[AE.INTPTXT]: src/Commons/Definitions/AEAD.lean#L173 -[AE.INTCTXT]: src/Commons/Definitions/AEAD.lean#L180 -[AE.Secure]: src/Commons/Definitions/AEAD.lean#L188 -[Encryption.Real]: src/Commons/Definitions/Encryption.lean#L71 +[real_ideal_distance_le]: src/Examples/AuthenticatedEncryption/Security.lean#L132 [SymmetricEncryption.encryptions]: src/Commons/Definitions/Encryption.lean#L65 -[BlockCipher]: src/Commons/Definitions/Cipher.lean#L29 -[AES-blockCipher]: src/Commons/Schemes/BlockCipher/AES.lean#L387 -[CTR]: src/Commons/Schemes/Stream/CTR.lean#L122 -[PMAC]: src/Commons/Schemes/MAC/PMAC.lean#L115 -[oracleStep]: src/Examples/AuthenticatedEncryption/Oracle.lean#L39 -[real_bisim]: src/Examples/AuthenticatedEncryption/Oracle.lean#L320 -[ptxt_bisim]: src/Examples/AuthenticatedEncryption/Oracle.lean#L103 -[cca_bisim]: src/Examples/AuthenticatedEncryption/Oracle.lean#L187 -[aeIdeal_bisim]: src/Examples/AuthenticatedEncryption/Oracle.lean#L240 -[encryptionReal_bisim]: src/Examples/AuthenticatedEncryption/Oracle.lean#L369 -[collision_mass_le]: src/Examples/AuthenticatedEncryption/Collision.lean#L54 -[hybrid_ideal_distance_le]: src/Examples/AuthenticatedEncryption/Collision.lean#L538 -[advantage_attach_le_win]: src/Examples/Games.lean#L107 -[win_attach_le]: src/Examples/Games.lean#L54 -[win_attach_comp_le]: src/Examples/Games.lean#L68 -[win_le_of_reduction]: src/Examples/Games.lean#L87 -[collision]: src/Examples/Games.lean#L149 -[collision_visible]: src/Examples/Games.lean#L154 -[collision_conditionallyEquivalent]: src/Examples/Games.lean#L158 -[collision_win_le]: src/Examples/Games.lean#L165 -[hybrid_ideal_advantage_le]: src/Examples/Games.lean#L190 -[attach_hybrid_ideal_advantage_le]: src/Examples/Games.lean#L209 +[AE.INDCCA]: src/Commons/Definitions/AEAD.lean#L165 [correctedChain]: src/Examples/AuthenticatedEncryption/Security.lean#L102 -[correctedChain_cca]: src/Examples/AuthenticatedEncryption/Security.lean#L121 -[correctedChain_ptxt]: src/Examples/AuthenticatedEncryption/Security.lean#L126 -[ae_of_ind_cca_int_ptxt]: src/Examples/AuthenticatedEncryption/Security.lean#L57 -[real_ideal_distance_le]: src/Examples/AuthenticatedEncryption/Security.lean#L132 -[construction_with_right_context]: src/Examples/Substitution.lean#L43 -[construction_with_left_context]: src/Examples/Substitution.lean#L70 -[constructsWithin_of_two_substitutions]: src/Examples/Substitution.lean#L120 -[Padding]: src/Examples/DSL/Components.lean#L86 -[WriteThrough]: src/Examples/DSL/Components.lean#L104 -[FirstRequests]: src/Examples/DSL/Components.lean#L116 -[AES-system]: src/Examples/DSL/AES.lean#L29 -[CBC]: src/Examples/DSL/AES.lean#L57 -[EncryptThenMAC]: src/Examples/DSL/AEAD.lean#L47 +[collision_mass_le]: src/Examples/AuthenticatedEncryption/Collision.lean#L54 [exists_pair_one_sub_supAgreement_le]: src/Probability/MultiCoupling.lean#L616 [not_supAgreement_disagreement_le_every_pair]: src/Probability/MultiCoupling.lean#L778 -[supAgreement]: src/Probability/MultiCoupling.lean#L87 -[supAgreement_eq_weight_overlapDist]: src/Probability/MultiCoupling.lean#L397 -[Distribution]: src/Probability/Distribution.lean#L56 -[ProbDist]: src/Probability/Distribution.lean#L149 -[isProbDist]: src/Probability/Distribution.lean#L128 -[mass]: src/Probability/Distribution.lean#L217 -[fTransform]: src/Probability/Distribution.lean#L632 -[prod]: src/Probability/Distribution.lean#L1005 -[pi]: src/Probability/Distribution.lean#L1646 -[bindK]: src/Probability/Kernel.lean#L49 -[bindK_bindK]: src/Probability/Kernel.lean#L95 -[bindK_single_comp]: src/Probability/Kernel.lean#L117 -[pi_eq_bindK_update]: src/Probability/Kernel.lean#L283 -[ProbDist.map]: src/Probability/Kernel.lean#L329 -[ProbDist.bind]: src/Probability/Kernel.lean#L341 -[uniform]: src/Probability/Distribution.lean#L566 -[statDist]: src/Probability/StatisticalDistance.lean#L88 -[statDist_triangle]: src/Probability/StatisticalDistance.lean#L243 -[statDist_fTransform_le]: src/Probability/StatisticalDistance.lean#L615 -[IsCoupling]: src/Probability/Coupling.lean#L46 -[statDist_le_offDiagonalMass]: src/Probability/Coupling.lean#L241 -[exists_coupling_offDiagonalMass_eq]: src/Probability/Coupling.lean#L320 -[expect]: src/Probability/Expectation.lean#L44 -[expect_add_left]: src/Probability/Expectation.lean#L66 -[expect_add_right]: src/Probability/Expectation.lean#L96 -[mass_ge_le_expect_div]: src/Probability/Expectation.lean#L199 -[expect_mul_sq_le_sq_mul_sq]: src/Probability/Expectation.lean#L215 -[ConvexOn.map_expect_le]: src/Probability/Expectation.lean#L297 -[statDist_eq_weight_posPart]: src/Probability/Lift.lean#L89 -[statDist_eq_weight_sub_weight_inf]: src/Probability/Lift.lean#L170 -[card_function_fiber_finset]: src/Probability/Counting.lean#L47 diff --git a/src/ConstructiveCryptography/DSL/GRAMMAR.md b/src/ConstructiveCryptography/DSL/GRAMMAR.md index 01b86bb..8a7134f 100644 --- a/src/ConstructiveCryptography/DSL/GRAMMAR.md +++ b/src/ConstructiveCryptography/DSL/GRAMMAR.md @@ -1,11 +1,17 @@ # Cryptographic component DSL This is a DSL embedded in Lean for the finite systems algebra. -The surface uses indentation, `←` for computation/assignment, `←$` for sampling, +The surface uses indentation, `←` for computation/assignment, `` ←$ `` for sampling, and `𝒰[T]` for the uniform law on a finite nonempty type. There are no braces, semicolons, `do` blocks, or combined assignment/bind operators in the surface. Lean remains the language for types, pure expressions, propositions, and proofs. +`interface`, `system`, `converter` and `filter` declarations compile to the typed systems and +typed converters of [Typed](../../RandomSystems/Typed/README.md) at every budget ([DSL][DSL]); +converters are declared as arrows of the [category of interfaces](../README.md#the-instances-on-interfaces), +so that components assemble with `≫` and `⊗ₘ`. Citations refer to the numbered +[references](../../../THEORY.md#references) of THEORY.md. + ## Grammar `block(P)` is a newline followed by one or more equally indented occurrences @@ -118,8 +124,8 @@ most once). the endomorphism `C.perPort : I.perPort q ⟶ I.perPort q`. - When the inside port has another declared interface `J`, each of whose labels one procedure calls, it is `C.perPort : I.perPort q ⟶ J.perPort (C.insideBudget q)`: the budget at an inside - label is that of the procedure calling it, and a procedure calling nothing needs none (Banfi's - `ρ^ctxt`, from `AE M C` to `Encryption M C`). + label is that of the procedure calling it, and a procedure calling nothing needs none (`ρ^ctxt` + of [9], from `AE M C` to `Encryption M C`). Its sources have the budget `C.bound * ∑ i, q i`. Other converters have no per-port typing. @@ -148,43 +154,81 @@ cost at most `q` need `q` inside queries. It is omitted when the count depends o replies or private bindings. A `filter F : I domain h ↦ P` gives `F : (I q).restrict P ⟶ I q` for every budget: it forwards -the queries of an admitted history and stops on the others (CR18 §3.4.3). The admitted +the queries of an admitted history and stops on the others [3, §3.4.3]. The admitted predicate must be closed under prefixes; `by` supplies a proof when the default tactic does not find one. ## Compilation -A component compiles to a deterministic program with sources of randomness: sampling stays in -the surface, and randomness enters the generated systems only through sources -(`TypedSystem.source`, Maurer 2002, Definition 1). +A component compiles to a deterministic [program][Program] with **sources** of randomness: +sampling stays in the surface, and randomness enters the generated systems only through +[sources][TypedSystem.source] of fresh samples of a closed law [4, Definition 1]. -- Every sampling statement `x ←$ P` becomes a call `x ← sample_k()` to a synthetic inside port - whose source draws fresh samples from `P`; the law is `C.law_k`. +- Every sampling statement `x ←$ P` [becomes a call][desugarSampling] `x ← sample_k()` to a + synthetic inside port whose source draws fresh samples from `P`; the law is `C.law_k`. - The body `C.body : Program (Option S) …` is a function of the inside exchanges of the current invocation, giving the next inside query or the reply and the new private bindings (a - deterministic automaton, Maurer 2002, Definition 2). Initialization runs in the first + deterministic automaton [4, Definition 2]). Initialization runs in the first invocation, when no bindings are stored yet; `S` is the type of `C.initial`, the initial bindings with each sample replaced by a value of its law. - Computation is ordinary `let` bindings; control flow is ordinary conditionals, pattern matching and list folds (`forEach`); a call is `callProg`, a reply `returnProg`. -- `C.program : I q ⟶ J (C.bound * q)` is the converter of the program +- `C.program : I q ⟶ J (C.bound * q)` is the [converter of the program][TypedConverter.ofProgram] (`TypedConverter.ofProgram`), on the outside domain of `I q`. - A converter is `C.program ≫ TypedConverter.rightContext J (C.randomness k)`: its program with - its sources attached beside the declared inside ports, each source at the inside budget `k`. A - converter that samples nothing is `C.program`. + its sources attached [beside][TypedConverter.rightContext] the declared inside ports, each + source at the inside budget `k`. A converter that samples nothing is `C.program`. - A system is `C.program • C.randomness k`. A system that samples nothing is the automaton of its program started in `C.initial`, `TypedSystem.ofAutomaton I step (single s)`. +The declarations generate typed systems and typed converters at every budget. An +[`interface I`][elabInterface] declaration generates `I q := Interface.queryBudget … q`, the +[query budget][Interface.queryBudget], and `I.perPort q := Interface.portBudget … q`, the +[per-port budget][Interface.portBudget]. A [`system S : I`][elabComponent] generates the typed +system `S : TypedSystem (I q)`, [compiled][elabProgramDecls] to `S.program • S.randomness k`: the +[converter of its program][TypedConverter.ofProgram] attached to its [sources][sourcesAt]. A +system that samples nothing is the [automaton][TypedSystem.ofAutomaton] of its program, and +a system without an exact domain [also gets][elabPerPortDecls] +`S.perPort : TypedSystem (I.perPort q)`. + +A [`converter C : I`][elabComponent] with `inside J` generates `C : I q ⟶ J (C.bound * q)`, +compiled to `C.program ≫ TypedConverter.rightContext J (C.randomness k)`: its program with its sources +[beside][TypedConverter.rightContext] the inside interface, or `C.program` when it samples nothing. With +a single inside interface it [also has a per-port typing][elabPerPortDecls] along a partial port +map `C.portMap : I.Port → Option J.Port`, through the +[converter of a port-preserving program][TypedConverter.ofPreservingProgram], with +`C.preserving` a proof of [`Program.PortPreserving`][Program.PortPreserving]. When `J` is `I` and +each procedure calls its own port, at most once, it is +`C.perPort : I.perPort q ⟶ I.perPort q`. When `J` is another interface, each of whose labels one +procedure calls at most once, it is `C.perPort : I.perPort q ⟶ J.perPort (C.insideBudget q)`: an +inside label has the budget of the procedure calling it, and a procedure calling nothing maps to +`none` and needs no inside budget, as in the [write-through cache][WriteThrough] and in +$`\rho^{ctxt}`$ and $`\rho^{ae}`$ of the +[authenticated encryption example](../../Examples/README.md#authenticated-encryption). When the +converter samples nothing and its number of inside calls is a function of the input, the +elaborator [also generates][elabExactDecls] +`C.exact : (I n).restrict (fun h => (h.map C.cost).sum ≤ q) ⟶ J q`, the +[converter of the costed program][TypedConverter.ofCostedProgram]. + +A [`filter F : I domain h ↦ P`][elabFilter] generates `F : (I q).restrict P ⟶ I q`, the +[filter][TypedConverter.filter] admitting `P`. + Attaching a program to a typed system runs its body against the system -(`Program.apply_ofProgram`, Maurer 2002, §3.3). A transcript of `C.program • R` has the mass of +(`Program.apply_ofProgram`, [4, §3.3]). A transcript of `C.program • R` has the mass of the system's deterministic systems on which the inlined program gives it (`TypedConverter.ofDDC_ofProgramOn_smul_ofPDS`). Sources are automata whose initial state is a -table of samples (`TypedSystem.ofAutomaton I step initial`, Maurer 2002, Definition 2, with the +table of samples (`TypedSystem.ofAutomaton I step initial`, [4, Definition 2], with the randomness in the initial state); parallel automata are the automaton of both -(`TypedSystem.parallel_ofAutomaton`), and a program attached to an automaton is the combined -automaton (`TypedConverter.ofProgram_smul_ofAutomaton`, `Program.combine`). Every compiled -component is therefore an automaton with a sampled initial state; bisimilar automata have the -same system (`automatonSystem_eq_of_bisim`). +(`TypedSystem.parallel_ofAutomaton`), and attaching a program to an automaton +[gives the combined automaton][TypedConverter.ofProgram_smul_ofAutomaton] (`Program.combine`), +also [for port-preserving programs][TypedConverter.ofPreservingProgram_smul_ofAutomaton]. Every +compiled component is therefore an automaton with a sampled initial state, and compiled systems +are compared by [bisimulation][automatonSystem_eq_of_bisim]: bisimilar automata have the same +system. The [memoryless source][MemorylessSource] `y ←$ ν; return y` +[is the memoryless system of `ν`][MemorylessSource.memoryless_eq], so systems built from programs +and memoryless sources are compared by the laws of one reply, through the composition laws of +[typed systems](../../RandomSystems/Typed/README.md#filters-contexts-sources-and-functional-systems): +each hop of [PRG length extension][ExPRG] is one rewrite. The assembly operators denote the existing CC operations. `α • R` applies a converter, `α ≫ β` composes converters, and `∥` and `⊗ₘ` compose systems and @@ -194,7 +238,7 @@ one component with multiple interfaces or by initialization enclosing all the shared behavior. A definition `system D ≔ e` takes its outside interface from the outermost component of `e`, at the implicit `budget`; the inner budgets follow from the converters' types. -The earlier proposed `attach A[ports] ↔ B[ports]` surface is not implemented. +There is no `attach A[ports] ↔ B[ports]` wiring form. The grammar above records the implemented DSL; it makes no claim that arbitrary feedback wiring can omit the existing domain and termination obligations. @@ -259,3 +303,60 @@ To check the DSL and its tests, run from the repository root: ```sh lake build Tests.DSL.Diagnostics Tests.DSL.Axioms ``` + +## Proof commands + +The proof commands are in `ConstructiveCryptography.Tactics`. +[`cc_normalize`][cc_normalize] rewrites attachments to normal forms, +[`cc_nonexpand`][cc_nonexpand] applies the compatibility laws, on interfaces also +[with the concrete parallel composition][cc_nonexpand-interfaces], [`cc_triangle`][cc_triangle] +takes a hybrid step, and [`cc_construct`][cc_construct] reduces a construction to its equality or +distance obligation. [`cc_calc relation`][cc_calc] proves $`X \simeq Y`$ from `=` and `≃` steps, +and [`cc_calc counted systems`][cc_calc-counted] builds an implication witness, whose uses +[`cc_usage`][cc_usage] counts. [`cc_calc statistical`][cc_calc-statistical] proves +$`d(X, Y) \le \sum_j \varepsilon_j`$ from `≈[ε]` steps, and +[`cc_calc mixed model using domination`][cc_calc-mixed] proves +$`X \simeq_{\sum_j \varepsilon_j} Y`$ from `≃[loss]` and `≈[ε]` steps. + + + +[DSL]: ../DSL.lean +[ExPRG]: ../../Examples/PRGLengthExtension.lean + + + +[Program]: ../../RandomSystems/Converter/Program.lean#L45 +[Program.PortPreserving]: ../../RandomSystems/Converter/Program.lean#L123 +[automatonSystem_eq_of_bisim]: ../../RandomSystems/System/Automaton.lean#L89 +[Interface.queryBudget]: ../../RandomSystems/Typed/Interface.lean#L63 +[Interface.portBudget]: ../../RandomSystems/Typed/Interface.lean#L74 +[TypedSystem.source]: ../../RandomSystems/Typed/Source.lean#L51 +[TypedSystem.ofAutomaton]: ../../RandomSystems/Typed/Automaton.lean#L42 +[TypedConverter.rightContext]: ../../RandomSystems/Typed/Context.lean#L109 +[TypedConverter.filter]: ../../RandomSystems/Typed/Filter.lean#L49 +[TypedConverter.ofProgram]: ../../RandomSystems/Typed/DSL/Converters.lean#L39 +[TypedConverter.ofCostedProgram]: ../../RandomSystems/Typed/DSL/Converters.lean#L51 +[TypedConverter.ofPreservingProgram]: ../../RandomSystems/Typed/DSL/Converters.lean#L68 +[TypedConverter.ofProgram_smul_ofAutomaton]: ../../RandomSystems/Typed/DSL/Converters.lean#L145 +[TypedConverter.ofPreservingProgram_smul_ofAutomaton]: ../../RandomSystems/Typed/DSL/Converters.lean#L155 +[desugarSampling]: Elaborator.lean#L194 +[elabInterface]: Elaborator.lean#L351 +[elabComponent]: Elaborator.lean#L811 +[elabProgramDecls]: Elaborator.lean#L644 +[elabPerPortDecls]: Elaborator.lean#L541 +[elabExactDecls]: Elaborator.lean#L716 +[elabFilter]: Elaborator.lean#L927 +[sourcesAt]: Elaborator.lean#L635 +[MemorylessSource]: ../../Commons/Definitions/Ideal.lean#L95 +[MemorylessSource.memoryless_eq]: ../../Commons/Definitions/Ideal.lean#L103 +[WriteThrough]: ../../Examples/DSL/Components.lean#L104 +[cc_normalize]: ../Tactics/Basic.lean#L30 +[cc_nonexpand]: ../Tactics/Categorical.lean#L166 +[cc_nonexpand-interfaces]: ../Notation.lean#L105 +[cc_triangle]: ../Tactics/Categorical.lean#L155 +[cc_construct]: ../Tactics/Categorical.lean#L42 +[cc_calc]: ../Tactics/Substitution.lean#L88 +[cc_calc-counted]: ../Tactics/Substitution.lean#L147 +[cc_usage]: ../Tactics/Substitution.lean#L243 +[cc_calc-statistical]: ../Tactics/Substitution.lean#L292 +[cc_calc-mixed]: ../Tactics/Substitution.lean#L295 diff --git a/src/ConstructiveCryptography/README.md b/src/ConstructiveCryptography/README.md new file mode 100644 index 0000000..3938c82 --- /dev/null +++ b/src/ConstructiveCryptography/README.md @@ -0,0 +1,416 @@ +# Constructive cryptography + +This library holds the abstract theory and its instances on interfaces. `CryptographicAlgebra` +defines the classes of assumptions, from resource theories to distinguisher classes and games; +`Specification` and `Construction` define specifications, constructions and relaxations over any +carrier; the instance files `InterfaceCategory`, `InterfaceMonoidal`, `InterfaceAlgebra` and +`InterfaceGame` instantiate the classes on interfaces; `Substitution` is the substitution +calculus; `Notation`, the proof commands of `Tactics` and the DSL front end +([GRAMMAR](DSL/GRAMMAR.md)) are built on these. The fields of the instances are the systems-level +objects of [RandomSystems](../RandomSystems/README.md), and the table of +[THEORY.md](../../THEORY.md#3-classes-and-instances) lists each field and axiom with its systems +object and theorem. Citations refer to the numbered [references](../../THEORY.md#references) of +THEORY.md. + +## The classes + +*The classes are assumptions: each introduces its notions (attachment, parallel +composition, distance, distinguishers, games, winners, solvers) only as fields and axioms, and +knows nothing about systems [3, §§4.4.3, 4.5.1, 4.7.2, 4.10–4.11], [6, §3], [7, §2.2], [8]. Only +the classes say "resource", for an element of $`\Phi A`$.* + +### `ResourceTheory C Φ`: attachment + +In the class [`ResourceTheory`][ResourceTheory], converters $`\alpha : A \to B`$ act on resources +$`R \in \Phi B`$: + +```math +\alpha R \in \Phi A, \qquad \mathrm{id}_A\, R = R, \qquad (\alpha \gg \beta)\, R = \alpha\,(\beta\, R) . +``` + +Attachment is the [contravariant functor][ResourceTheory.functor] +$`\Phi : C^{\mathrm{op}} \to \mathrm{Type}`$. + +### `CryptographicAlgebra C Φ`: parallel composition + +The class [`CryptographicAlgebra`][CryptographicAlgebra] is a lax monoidal structure on $`\Phi`$: +resources [compose in parallel][CA.parallel], with the [dummy resource][CA.dummy] as unit. + +```math +R \parallel S \in \Phi(A \otimes B), \qquad \mathbf 1 \in \Phi(\mathbb I), \qquad +(\alpha \otimes \beta)(R \parallel S) = \alpha R \parallel \beta S . +``` + +Derived: [locality][CA.attach_parallel], [associativity][CA.parallel_assoc], and the +[left][CA.parallel_dummy_left] and [right][CA.parallel_dummy_right] unit laws. + +### `CompatiblePseudoMetric C Φ`: distance + +The class [`CompatiblePseudoMetric`][CompatiblePseudoMetric] adds a pseudo-metric $`d`$, the +[distance][CA.distance], on each $`\Phi A`$ [6, Definition 2], [8, Definition 2]: + +```math +d(\alpha R, \alpha S) \le d(R, S), \qquad +d(R \parallel R',\ S \parallel S') \le d(R, S) + d(R', S') . +``` + +Derived: [attachment is non-expanding][distance_attach_le] and +[parallel composition adds distances][distance_parallel_le]. For interfaces the metric comes from +the distinguisher class below. + +### `CompatibleDistinguisherClass C Φ`: distinguishers + +The class [`CompatibleDistinguisherClass`][CompatibleDistinguisherClass] has a class +$`\mathcal D_A`$ of maps $`\Phi A \to \mathbb R`$, closed under absorbing a converter and under running +a fixed resource beside, whose [advantage distance][advantageDistance] is the metric [8, §4.5]: + +```math +d(R, S) = \sup_{D \in \mathcal D_A} \lvert D(R) - D(S) \rvert, \qquad +D \in \mathcal D_A \;\Longrightarrow\; D(\alpha\,\cdot\,) \in \mathcal D_B,\ \ D(\,\cdot \parallel T),\ D(T \parallel \cdot\,) \in \mathcal D . +``` + +**Closure gives compatibility** [8, Lemma 1]: the advantage distance of a closed class +[is a compatible pseudo-metric][CompatibleDistinguisherClass.ofClosure]. + +### `Games C Game` and `DistinctionGames C Φ Game`: games, and games related to distinguishing + +The class [`Games`][Games] is the abstraction of [3, §4.4.3, §4.5.1 and §4.7.2]. A problem is a +set of solvers with a performance function [3, Definition 4.2]; for a game the solvers are +winners and the performance is the winning probability [3, Definition 4.5], so a winner is given +by its winning probability $`W : \mathrm{Game}\,A \to \mathbb R`$ for each game. The class has games +$`\mathrm{Game}\,A`$ on each object, attachment $`\alpha \cdot G`$ of converters to games, +contravariant in serial composition, and a set $`\mathcal W_A`$ of winners closed under +[absorbing][Games.absorb] a converter, $`\omega(w c, g) = \omega(w, c g)`$ [3, §4.7.2, +equation (4.9)]. Games and winners do not involve resources: + +```math +\mathrm{id} \cdot G = G, \qquad (\alpha \beta) \cdot G = \alpha \cdot (\beta \cdot G), \qquad +W \in \mathcal W_A \;\Longrightarrow\; W(\alpha \cdot\,\cdot\,) \in \mathcal W_B . +``` + +Absorbing a serial composition [absorbs its converters in turn][Games.absorb_comp]. + +The class [`DistinctionGames`][DistinctionGames], extending `Games`, is the abstraction of +[3, §§4.10–4.11], relating games and distinction problems. Its solvers are the objects that are +both a distinguisher and a winner, as $`D`$ in [3, Lemma 4.16]: a set $`\mathcal S_A`$ of pairs +$`(D, W)`$ of a decision probability $`D : \Phi A \to \mathbb R`$ and a winning probability $`W`$, which +is a winner, closed under [absorbing][DistinctionGames.absorb] a converter [3, §4.7.2]. It has the visible +resource $`G^-`$ of a game [3, Definition 4.18], with which attachment commutes since a converter +neither sees nor affects the MBO [3, §4.7.2], and a conditional equivalence +$`G \mathrel{|\!\equiv} T`$ of games to resources [3, Definition 4.19], under which each solver's advantage is at most its winning +probability [3, Lemma 4.16 and the proof of Theorem 4.17]: + +```math +(D, W) \in \mathcal S_A \;\Longrightarrow\; W \in \mathcal W_A, \qquad +(\alpha \cdot G)^- = \alpha\, G^-, \qquad +G \mathrel{|\!\equiv} T,\ (D, W) \in \mathcal S_A \;\Longrightarrow\; \lvert D(G^-) - D(T) \rvert \le W(G) . +``` + +## The instances on interfaces + +Interfaces are an instance of each class: the carrier $`\Phi A`$ is the +[typed systems](../RandomSystems/Typed/README.md) on $`A`$, every field is a systems-level object, +and every axiom is discharged by a systems-level theorem. The instances are +[`Interface.category`][Interface.category], [`Interface.monoidal`][Interface.monoidal], +[`Interface.resourceTheory`][Interface.resourceTheory], +[`Interface.cryptographicAlgebra`][Interface.cryptographicAlgebra], +[`Interface.compatibleDistinguisherClass`][Interface.compatibleDistinguisherClass], +[`Interface.games`][Interface.games] and [`Interface.distinctionGames`][Interface.distinctionGames]; +the table of [THEORY.md](../../THEORY.md#3-classes-and-instances) gives each field and axiom. + +Interfaces and typed converters form a category under serial composition, and a monoidal +category under parallel composition. In the notation of the category, the attachment laws read +[`Interface.identity_attach`][Interface.identity_attach] and +[`Interface.comp_smul`][Interface.comp_smul]. The abstract [parallel composition][Interface.cc_parallel_eq] +and [dummy][Interface.cc_dummy_eq] are the systems-level ones, and the metric +[is the transcript distance][Interface.cc_distance_eq] of +[Distance](../RandomSystems/Distance/README.md): + +```math +d(R, S) = \Delta(R, S) = \sup_P \mathrm{Adv}_P(R, S) . +``` + +Interfaces are an instance of both games classes, and the instance is the only place where they +meet random systems: its games are the [typed games](../RandomSystems/Typed/README.md#typed-games), +MBO random systems as [3, §3.7.1] instantiates games, and its winners and solvers are +probabilistic distinguishers, through their [solver behaviors][Domain.SolverBehavior]. A bound on +the winning probability of every distinguisher +[bounds the winning probability of every winner][Interface.win_le]. A typed game conditionally +equivalent to a typed system $`T`$, $`G \mathrel{|\!\equiv} T`$, whose MBO stays unset with +probability at least $`1 - \varepsilon`$ on fixed queries, +[has its visible typed system within][Interface.dist_visible_le] $`\varepsilon`$ of $`T`$, +$`\Delta(G^-, T) \le \varepsilon`$ [3, Theorem 4.17]. A presented typed game is conditionally +equivalent to a typed system [exactly when][Interface.conditionallyEquivalent_ofPDG_iff] the game +it presents on random systems is; if it is conditionally equivalent to $`S`$ and the condition +holds with probability at most $`\varepsilon`$ on the empty and every admitted query sequence, the +presented typed system $`R`$ is [within][Interface.game_dist_le] $`\varepsilon`$ of $`S`$, +$`\Delta(R, S) \le \varepsilon`$. + +## Notation + +With `open scoped SystemAlgebra`: [`Δ R S`][notation-distance] for the distance of +`CompatiblePseudoMetric`, [`R ∥ S`][notation-parallel] for `TypedSystem.parallel`, +[`𝓡 —[π]→ 𝒮`][notation-constructs] for $`\mathcal R \xrightarrow{\pi} \mathcal S`$ and +[`𝓡 —[π; ε]→ 𝒮`][notation-constructsWithin] for +$`\mathcal R \xrightarrow{\pi,\ \varepsilon} \mathcal S`$ (constructions, below), +[`G |≡ T`][notation-conditionallyEquivalent] for $`G \mathrel{|\!\equiv} T`$, and +[`R ≃[ε] S`][notation-substitutes] for substitution within $`\varepsilon`$ (the substitution +calculus, below). + +## Specifications and constructions + +*A specification is a set of resources; a converter constructs one specification from another +[6, §§2–4]. The carrier-free notions hold for any map; the others are stated on the classes +above.* + +```math +\mathcal R \xrightarrow{\ \pi\ } \mathcal S \;:\iff\; \pi\mathcal R \subseteq \mathcal S, +\qquad +\mathcal R \xrightarrow{\ \pi,\ \varepsilon\ } \mathcal S \;:\iff\; +\forall R \in \mathcal R\ \exists S \in \mathcal S.\ d(\pi R, S) \le \varepsilon . +``` + +A [**specification**][Specification] is a set; [exact][Specification.Constructs] and +[approximate][Specification.ConstructsWithin] construction are as above, for any map. On a +cryptographic algebra the map is attachment, giving [exact][CA.Specification.Constructs] and +[approximate][CA.Specification.ConstructsWithin] construction by a converter. Constructions +compose serially [6, Lemma 1], +$`\mathcal R \xrightarrow{\pi_2} \mathcal S \xrightarrow{\pi_1} \mathcal T \Rightarrow \mathcal R \xrightarrow{\pi_1 \gg \pi_2} \mathcal T`$, +[exactly][Constructs.serial] and [approximately][ConstructsWithin.serial] with added errors, and in +parallel, $`\mathcal R \parallel \mathcal R' \xrightarrow{\pi \otimes \pi'} \mathcal S \parallel \mathcal S'`$, +[exactly][Constructs.parallel] and [approximately][ConstructsWithin.parallel]. + +A [**relaxation**][Relaxation] maps each $`R`$ to a set $`\mathcal R' \ni R`$, lifted to +specifications by union. A relaxation is [compatible][Relaxation.Compatible] when +[it preserves construction][Relaxation.compatible_iff], and compatible relaxations +[pass through serial constructions][Constructs.relax_serial]. The +[**ε-relaxation**][epsilonRelaxation] +$`\mathcal R^\varepsilon = \lbrace R' \mid \exists R \in \mathcal R.\ d(R, R') \le \varepsilon \rbrace`$ +[turns approximate construction into exact construction][constructs_epsilonRelaxation_iff], +$`\mathcal R \xrightarrow{\pi} \mathcal S^\varepsilon \iff \mathcal R \xrightarrow{\pi,\ \varepsilon} \mathcal S`$, +and its errors [add under serial composition][Constructs.serial_epsilonRelaxation]. + +The [**star relaxation**][CA.star] [6, §3.4, Lemma 3] +$`\mathcal R^{*} = \lbrace \sigma R \mid \sigma \in \Sigma,\ R \in \mathcal R \rbrace`$ is +[idempotent][star_idem], a [closure operator][starClosure], and +[exact construction survives star-relaxing both ends][Constructs.star] for a converter commuting +with the class. A [**simulator**][constructs_of_simulator] [6, Lemma 5] $`\sigma \in \Sigma`$ with +$`d(\pi R, \sigma S) \le \varepsilon`$ gives +$`\lbrace R \rbrace \xrightarrow{\pi} (\lbrace S \rbrace^{*})^{\varepsilon}`$. Other relaxations and +judgments are the [kernel relaxation][kernel] of a map, [test-bounded specifications][gameSpec], +and [constructibility][Constructible] by a class of constructors. + +## The substitution calculus + +*Stated over any [`ResourceTheory`][ResourceTheory] [9, Chapter 2 and §4.1.4], +[7, Definitions 2.2.6–2.2.9 and Theorem 2.2.10].* + +### Substitution relations and implication witnesses + +A [**substitution relation**][SubstitutionRelation] $`\simeq`$ relates resources on one +interface [9, Definition 2.3.1]: + +```math +S \simeq T \Rightarrow T \simeq S, \qquad S \simeq T \simeq U \Rightarrow S \simeq U, \qquad +S \simeq T \Rightarrow \rho S \simeq \rho T . +``` + +An [**implication witness**][Implication] from assumptions $`S_i \simeq T_i`$ to a target +$`X \simeq Y`$ is a chain [9, §2.3.1]: + +```math +X = \rho_0 S_{i_0}^{b_0} \simeq \rho_0 S_{i_0}^{\lnot b_0} = \rho_1 S_{i_1}^{b_1} \simeq \cdots \simeq \rho_k S_{i_k}^{\lnot b_k} = Y . +``` + +A witness [counts the uses][Implication.usageCount] of each assumption. The hybrid argument +[9, Lemma 2.3.2] holds [for a substitution relation][substitutes_of_hybrid] and +[for distances][distance_hybrid_le]. A witness [is valid][Implication.substitutes], taking valid +assumptions to its target, and [distances add][Implication.distance_le] along it. Witnesses can be +[transformed by a converter][Implication.map], [reversed][Implication.reverse] and +[appended][Implication.append], and [use counts add][usageCount_append] under appending. The +derivable targets form the [generated relation][generatedRelation], and they +[hold in every substitution relation satisfying the assumptions][derivable_substitutes]. + +### Distinguisher-indexed substitution + +A [**distinguisher advantage**][DistinguisherAdvantage] gives admitted distinguishers +$`\mathcal D_A`$ and an advantage $`\Delta_D`$, a pseudo-distance for each $`D`$. +[Substitution within an error *function*][SubstitutesWithin] [9, §2.3.3]: + +```math +S \simeq_{\varepsilon} T \;:\iff\; \forall D \in \mathcal D_A.\ \Delta_D(S, T) \le \varepsilon(D) . +``` + +Substitution is [symmetric][SubstitutesWithin.symm], and [errors add][SubstitutesWithin.trans]: +$`S \simeq_\varepsilon T \simeq_{\varepsilon'} U \Rightarrow S \simeq_{\varepsilon + \varepsilon'} U`$. +A statistical step gives a substitution within a constant error, +[from a distance bound][SubstitutesWithin.of_distance] $`d(S, T) \le \varepsilon`$ when +$`\Delta_D \le d`$, and more generally +[from any statistical bound dominating the advantage][SubstitutesWithin.of_statistical]. Reduction [9, p. 16], +$`S \simeq_\varepsilon T \Rightarrow \rho S \simeq_{\varepsilon(\cdot \circ \rho)} \rho T`$, +transports substitutions [through one converter][SubstitutesWithin.attach] and +[through a serial composition][SubstitutesWithin.attach_serial]. In mixed chains +[7, Theorem 2.2.10], the [assumption uses][Implication.substitutesWithin] and the +[statistical steps][Implication.substitutesWithin_of_mixed] along a witness add up. + +**On interfaces.** [`DistinguisherAdvantage`][DistinguisherAdvantage] is a structure, and for every +class of admitted distinguishers [`Interface.distinguisherAdvantage`][Interface.distinguisherAdvantage] +is one, with carrier $`\Phi A :=`$ `TypedSystem A`: its distinguishers are the systems-level +[distinguisher behaviors][Domain.DistinguisherBehavior], its field `admissible` is that class, its +field `advantage` is the systems-level +[advantage][DistinguisherBehavior.advantage], and its laws `advantage_self`, `advantage_symm` and +`advantage_triangle` are the systems-level [zero][DistinguisherBehavior.advantage_self], +[symmetry][DistinguisherBehavior.advantage_symm] and +[triangle][DistinguisherBehavior.advantage_triangle] laws. + +A converter $`\alpha`$ absorbed into a distinguisher is the reduction of a security proof [3]: +the systems-level [absorption][DistinguisherBehavior.absorb] gives $`D \circ \alpha`$, and absorbing +a serial composition [absorbs its converters in turn][DistinguisherBehavior.absorb_comp], +$`D \circ (\alpha \gg \beta) = (D \circ \alpha) \circ \beta`$. Hence an advantage between attachments +[is the advantage with the converter absorbed][Interface.distinguisherAdvantage_attach], +$`\mathrm{Adv}_D(\alpha R, \alpha S) = \mathrm{Adv}_{D \circ \alpha}(R, S)`$; every advantage +[is at most the distance][Interface.distinguisherAdvantage_le_distance], $`\mathrm{Adv}_D \le \Delta`$, +by the [systems-level bound][DistinguisherBehavior.advantage_le_transcriptDistance]; and +substitutions [transport through converters][Interface.substitutesWithin_attach] when the class is +closed under absorbing converters. The class +[`Interface.AdmissibleDistinguishers`][Interface.AdmissibleDistinguishers] +bundles the admitted distinguishers with that closure; for its instance in scope, +$`R \simeq_\varepsilon S`$ is written [`R ≃[ε] S`][notation-substitutes] (scoped in +`SystemAlgebra`), substitutions +[transport through every converter][AdmissibleDistinguishers.substitutesWithin_attach], and every +security notion of Commons is stated this way. + +### Substitution relaxations and constructions + +The [**substitution image**][substitutionImage] collects the transformed endpoints of a one-use +substitution [9, §4.1.4] and gives a [relaxation][singleSubstitutionRelaxation]. The +[**substitution relaxation**][substitutionRelaxation] of a specification is the resources +substituting for a member; it is [compatible with converters][substitutionRelaxation_compatible] +and [idempotent][substitutionRelaxation_idem]. Constructions with simulators +compose [9, Definition 2.4.3 and Theorem 2.4.4]: a witness +[gives serial simulators][Implication.exists_serial_simulators], and +[derivable constructions compose serially][Constructs.derivable_serial_simulators]. + + + +[ResourceTheory]: CryptographicAlgebra/Basic.lean#L50 +[ResourceTheory.functor]: CryptographicAlgebra/Basic.lean#L69 +[CryptographicAlgebra]: CryptographicAlgebra/Basic.lean#L97 +[CA.parallel]: CryptographicAlgebra/Basic.lean#L126 +[CA.dummy]: CryptographicAlgebra/Basic.lean#L134 +[CA.attach_parallel]: CryptographicAlgebra/Basic.lean#L160 +[CA.parallel_assoc]: CryptographicAlgebra/Basic.lean#L182 +[CA.parallel_dummy_left]: CryptographicAlgebra/Basic.lean#L196 +[CA.parallel_dummy_right]: CryptographicAlgebra/Basic.lean#L211 +[CompatiblePseudoMetric]: CryptographicAlgebra/PseudoMetric.lean#L43 +[CA.distance]: CryptographicAlgebra/PseudoMetric.lean#L63 +[distance_attach_le]: CryptographicAlgebra/PseudoMetric.lean#L90 +[distance_parallel_le]: CryptographicAlgebra/PseudoMetric.lean#L145 +[advantageDistance]: CryptographicAlgebra/Distinguisher.lean#L36 +[CompatibleDistinguisherClass]: CryptographicAlgebra/Distinguisher.lean#L77 +[CompatibleDistinguisherClass.ofClosure]: CryptographicAlgebra/Distinguisher.lean#L102 +[Games]: CryptographicAlgebra/Game.lean#L62 +[Games.absorb]: CryptographicAlgebra/Game.lean#L93 +[Games.absorb_comp]: CryptographicAlgebra/Game.lean#L101 +[DistinctionGames]: CryptographicAlgebra/Game.lean#L112 +[DistinctionGames.absorb]: CryptographicAlgebra/Game.lean#L148 + + + +[Interface.category]: InterfaceCategory.lean#L30 +[Interface.identity_attach]: InterfaceCategory.lean#L45 +[Interface.comp_smul]: InterfaceCategory.lean#L50 +[Interface.monoidal]: InterfaceMonoidal.lean#L162 +[Interface.resourceTheory]: InterfaceAlgebra.lean#L71 +[Interface.cryptographicAlgebra]: InterfaceAlgebra.lean#L142 +[Interface.compatibleDistinguisherClass]: InterfaceAlgebra.lean#L181 +[Interface.cc_parallel_eq]: InterfaceAlgebra.lean#L188 +[Interface.cc_dummy_eq]: InterfaceAlgebra.lean#L192 +[Interface.cc_distance_eq]: InterfaceAlgebra.lean#L196 +[Interface.games]: InterfaceGame.lean#L69 +[Interface.distinctionGames]: InterfaceGame.lean#L125 +[Domain.SolverBehavior]: ../RandomSystems/Game/MBOAttachment.lean#L2169 +[Interface.win_le]: InterfaceGame.lean#L170 +[Interface.dist_visible_le]: InterfaceGame.lean#L186 +[Interface.conditionallyEquivalent_ofPDG_iff]: InterfaceGame.lean#L200 +[Interface.game_dist_le]: InterfaceGame.lean#L213 +[notation-distance]: Notation.lean#L24 +[notation-parallel]: Notation.lean#L28 +[notation-constructs]: Notation.lean#L31 +[notation-constructsWithin]: Notation.lean#L35 +[notation-substitutes]: Notation.lean#L41 +[notation-conditionallyEquivalent]: Notation.lean#L47 + + + +[Specification]: Specification/Defs.lean#L18 +[Specification.Constructs]: Specification/Basic.lean#L31 +[Specification.ConstructsWithin]: Specification/Metric.lean#L23 +[CA.Specification.Constructs]: CryptographicAlgebra/Basic.lean#L368 +[CA.Specification.ConstructsWithin]: CryptographicAlgebra/PseudoMetric.lean#L179 +[Constructs.serial]: CryptographicAlgebra/Basic.lean#L443 +[ConstructsWithin.serial]: CryptographicAlgebra/PseudoMetric.lean#L234 +[Constructs.parallel]: CryptographicAlgebra/Basic.lean#L518 +[ConstructsWithin.parallel]: CryptographicAlgebra/PseudoMetric.lean#L254 +[Relaxation]: Specification/Relaxation/Defs.lean#L22 +[Relaxation.Compatible]: CryptographicAlgebra/Relaxation.lean#L46 +[Relaxation.compatible_iff]: CryptographicAlgebra/Relaxation.lean#L84 +[Constructs.relax_serial]: CryptographicAlgebra/Relaxation.lean#L136 +[epsilonRelaxation]: CryptographicAlgebra/Epsilon.lean#L43 +[constructs_epsilonRelaxation_iff]: CryptographicAlgebra/Epsilon.lean#L165 +[Constructs.serial_epsilonRelaxation]: CryptographicAlgebra/Epsilon.lean#L225 +[CA.star]: CryptographicAlgebra/Star.lean#L59 +[star_idem]: CryptographicAlgebra/Star.lean#L94 +[starClosure]: Specification/Star.lean#L55 +[Constructs.star]: CryptographicAlgebra/Star.lean#L145 +[constructs_of_simulator]: CryptographicAlgebra/Star.lean#L269 +[kernel]: Specification/Relaxation/Kernel.lean#L16 +[gameSpec]: Specification/Game/Basic.lean#L24 +[Constructible]: Construction/Defs.lean#L24 + + + +[SubstitutionRelation]: Substitution/Basic.lean#L45 +[Implication]: Substitution/Basic.lean#L176 +[Implication.usageCount]: Substitution/Basic.lean#L207 +[substitutes_of_hybrid]: Substitution/Basic.lean#L77 +[distance_hybrid_le]: Substitution/Basic.lean#L120 +[Implication.substitutes]: Substitution/Basic.lean#L214 +[Implication.distance_le]: Substitution/Basic.lean#L254 +[Implication.map]: Substitution/Implication.lean#L127 +[Implication.reverse]: Substitution/Implication.lean#L158 +[Implication.append]: Substitution/Implication.lean#L207 +[usageCount_append]: Substitution/Implication.lean#L275 +[generatedRelation]: Substitution/Implication.lean#L309 +[derivable_substitutes]: Substitution/Implication.lean#L335 +[DistinguisherAdvantage]: Substitution/Reduction.lean#L46 +[SubstitutesWithin]: Substitution/Reduction.lean#L72 +[SubstitutesWithin.symm]: Substitution/Reduction.lean#L80 +[SubstitutesWithin.trans]: Substitution/Reduction.lean#L94 +[SubstitutesWithin.of_distance]: Substitution/Reduction.lean#L127 +[SubstitutesWithin.of_statistical]: Substitution/Reduction.lean#L110 +[SubstitutesWithin.attach]: Substitution/Reduction.lean#L145 +[SubstitutesWithin.attach_serial]: Substitution/Reduction.lean#L175 +[Implication.substitutesWithin]: Substitution/Quantitative.lean#L49 +[Implication.substitutesWithin_of_mixed]: Substitution/Quantitative.lean#L105 +[Interface.distinguisherAdvantage]: InterfaceAlgebra.lean#L208 +[Domain.DistinguisherBehavior]: ../RandomSystems/Distance/Distinguisher.lean#L207 +[DistinguisherBehavior.advantage]: ../RandomSystems/Distance/Distinguisher.lean#L218 +[DistinguisherBehavior.advantage_self]: ../RandomSystems/Distance/Distinguisher.lean#L228 +[DistinguisherBehavior.advantage_symm]: ../RandomSystems/Distance/Distinguisher.lean#L230 +[DistinguisherBehavior.advantage_triangle]: ../RandomSystems/Distance/Distinguisher.lean#L233 +[DistinguisherBehavior.advantage_le_transcriptDistance]: ../RandomSystems/Distance/Distinguisher.lean#L238 +[DistinguisherBehavior.absorb]: ../RandomSystems/Distance/Distinguisher.lean#L291 +[DistinguisherBehavior.absorb_comp]: ../RandomSystems/Distance/Distinguisher.lean#L304 +[Interface.distinguisherAdvantage_attach]: InterfaceAlgebra.lean#L220 +[Interface.distinguisherAdvantage_le_distance]: InterfaceAlgebra.lean#L280 +[Interface.substitutesWithin_attach]: InterfaceAlgebra.lean#L231 +[Interface.AdmissibleDistinguishers]: InterfaceAlgebra.lean#L246 +[AdmissibleDistinguishers.substitutesWithin_attach]: InterfaceAlgebra.lean#L255 +[substitutionImage]: Substitution/Relaxation.lean#L45 +[singleSubstitutionRelaxation]: Substitution/Relaxation.lean#L59 +[substitutionRelaxation]: Substitution/Relaxation.lean#L164 +[substitutionRelaxation_compatible]: Substitution/Relaxation.lean#L182 +[substitutionRelaxation_idem]: Substitution/Relaxation.lean#L202 +[Implication.exists_serial_simulators]: Substitution/Construction.lean#L44 +[Constructs.derivable_serial_simulators]: Substitution/Construction.lean#L107 diff --git a/src/Examples/README.md b/src/Examples/README.md new file mode 100644 index 0000000..687cf5f --- /dev/null +++ b/src/Examples/README.md @@ -0,0 +1,141 @@ +# Examples + +This library holds worked examples: the security of authenticated encryption from ind-cca and +int-ptxt, with its collision bound and its collision game ([`AuthenticatedEncryption`](AuthenticatedEncryption)); +hardness and game hops in every instance of the games classes ([Games][ExGames]); substitutions +on interfaces ([Substitution][ExSub]); PRG length extension, proved by the laws of one reply of +memoryless systems ([PRGLengthExtension][ExPRG]); components, AES and an AEAD written in the DSL +([`DSL`](DSL)); and the proof commands on interfaces ([Usability][ExUse]). Citations refer to the +numbered [references](../../THEORY.md#references) of THEORY.md. + +## Authenticated encryption + +The security of authenticated encryption [9, Theorem 2.3.10(4)], corrected, is in +[Security][AESec]. Let $`R`$ be the real system [`AE.Real`][AE.Real], $`E`$ the encryption oracle +[`Encryption.Real`][Encryption.Real], and $`I = \rho^{ae} E`$ the ideal system +(`AE.Ideal • Encryption.Real`): [`AE.Ideal`][AE.Ideal], like [`AE.CTXT`][AE.CTXT] +($`\rho^{ctxt}`$), is a converter from [`AE M C`][AE] to [`Encryption M C`][Encryption]. Let $`P`$ and $`C`$ be the +[plaintext filter][AE.PTXT] `AE.PTXT` and the [random-message transformation][AE.CCA] `AE.CCA`, +and $`q = (q_e, q_d)`$ the budgets per port. The corrected chain uses each assumption twice: + +```math +R \;\simeq_{\mathrm{ptxt}}\; P R \;\simeq_{\mathrm{cca}}\; P C R \;\simeq_{\mathrm{ptxt}}\; P C P R \;\simeq_{\mathrm{cca}}\; P C P C R \;\approx_{q_e^2 / \lvert \mathcal M \rvert}\; I . +``` + +The last step is the [collision bound][hybrid_ideal_distance_le], which compares the hybrid +with `AE.Ideal.perPort • Encryption.Real.perPort` ([Collision][AECol]). The results are the +[counted witness][correctedChain], with [two uses of ind-cca][correctedChain_cca] and +[two of int-ptxt][correctedChain_ptxt], the [advantage form][ae_of_ind_cca_int_ptxt], and the +[distance form][real_ideal_distance_le] +$`\Delta(R, I) \le 2\,\Delta(R, P R) + 2\,\Delta(R, C R) + q_e^2 / \lvert \mathcal M \rvert`$. +The systems and the notions [`AE.INDCCA`][AE.INDCCA], [`AE.INTPTXT`][AE.INTPTXT], +[`AE.INTCTXT`][AE.INTCTXT] and [`AE.Secure`][AE.Secure] are Commons definitions +([AEAD][AEDefs]); int-ctxt and ae read $`R \simeq \rho^{ctxt} E`$ and $`R \simeq \rho^{ae} E`$. +The systems are compared as [oracle automata][oracleStep] ([Oracle][AEOracle], +[Hybrid][AEHybrid]), each by a bisimulation of its compiled automaton: the +[real system][real_bisim], the [encryption oracle][encryptionReal_bisim], and the images under +the [plaintext filter][ptxt_bisim], the [random-message transformation][cca_bisim] and the +[ideal transformation][aeIdeal_bisim]. + +## Games + +The examples are in [Games][ExGames]. In every instance of `Games`: hardness through +[a reduction][win_attach_le], [two reductions][win_attach_comp_le] and +[a lossy reduction][win_le_of_reduction], $`W(G_1) \le k\, W(\alpha \cdot G_2) \le k\, \varepsilon`$, +the shape of a reduction that guesses one of $`k`$ sessions. In every instance of +`DistinctionGames`: a [game hop inside a construction][advantage_attach_le_win], +$`\lvert D(\alpha\, G^-) - D(\alpha T) \rvert \le W(\alpha \cdot G)`$ for $`G \mathrel{|\!\equiv} T`$. +On interfaces, the collision game of authenticated encryption +[is the game the collision discrete game presents][collision], with +[visible typed system the hybrid][collision_visible] and +[conditionally equivalent to the ideal][collision_conditionallyEquivalent]; every winner +[wins it with probability at most][collision_win_le] $`q_e^2 / \lvert \mathcal M \rvert`$, so +every solver's advantage between the hybrid and the ideal +[is at most][hybrid_ideal_advantage_le] $`q_e^2 / \lvert \mathcal M \rvert`$, also +[inside any construction][attach_hybrid_ideal_advantage_le]. + +## Substitutions on interfaces + +[Substitution][ExSub] gives single substitutions with a context +[on the right][construction_with_right_context] or [on the left][construction_with_left_context], +and [two statistical substitutions][constructsWithin_of_two_substitutions] giving +$`\lbrace R \rbrace \xrightarrow{\pi,\ \varepsilon_1 + \varepsilon_2} \lbrace \sigma S \rbrace`$. + +## DSL components + +[Components][ExComp] declares counters, fresh and persistent randomness, a +[padding converter][Padding] with an inferred cost, the [write-through cache][WriteThrough] +typed by a partial port map, and a [filter][FirstRequests]. + +## AES and AEAD in the DSL + +[AES][ExAES] and [AEAD][ExAEAD] declare [AES-256][AES-system] as a system +with a random key, from the Commons [block cipher][BlockCipher] [AES][AES-blockCipher], with +converters around it such as [CBC-MAC][CBC]; and [AES-CTR followed by PMAC][EncryptThenMAC], +from the Commons [CTR][CTR] and [PMAC][PMAC] converters. The proof commands on interfaces are +exercised in [Usability][ExUse]. + + + +[AEDefs]: ../Commons/Definitions/AEAD.lean +[AEOracle]: AuthenticatedEncryption/Oracle.lean +[AEHybrid]: AuthenticatedEncryption/Hybrid.lean +[AECol]: AuthenticatedEncryption/Collision.lean +[AESec]: AuthenticatedEncryption/Security.lean +[ExSub]: Substitution.lean +[ExGames]: Games.lean +[ExComp]: DSL/Components.lean +[ExAES]: DSL/AES.lean +[ExAEAD]: DSL/AEAD.lean +[ExUse]: Usability.lean +[ExPRG]: PRGLengthExtension.lean + + + +[AE.Real]: ../Commons/Definitions/AEAD.lean#L54 +[AE]: ../Commons/Definitions/AEAD.lean#L37 +[Encryption]: ../Commons/Definitions/Encryption.lean#L54 +[AE.CCA]: ../Commons/Definitions/AEAD.lean#L65 +[AE.PTXT]: ../Commons/Definitions/AEAD.lean#L84 +[AE.CTXT]: ../Commons/Definitions/AEAD.lean#L98 +[AE.Ideal]: ../Commons/Definitions/AEAD.lean#L111 +[AE.INDCCA]: ../Commons/Definitions/AEAD.lean#L165 +[AE.INTPTXT]: ../Commons/Definitions/AEAD.lean#L173 +[AE.INTCTXT]: ../Commons/Definitions/AEAD.lean#L180 +[AE.Secure]: ../Commons/Definitions/AEAD.lean#L188 +[Encryption.Real]: ../Commons/Definitions/Encryption.lean#L71 +[BlockCipher]: ../Commons/Definitions/Cipher.lean#L29 +[AES-blockCipher]: ../Commons/Schemes/BlockCipher/AES.lean#L387 +[CTR]: ../Commons/Schemes/Stream/CTR.lean#L122 +[PMAC]: ../Commons/Schemes/MAC/PMAC.lean#L115 +[oracleStep]: AuthenticatedEncryption/Oracle.lean#L39 +[real_bisim]: AuthenticatedEncryption/Oracle.lean#L320 +[ptxt_bisim]: AuthenticatedEncryption/Oracle.lean#L103 +[cca_bisim]: AuthenticatedEncryption/Oracle.lean#L187 +[aeIdeal_bisim]: AuthenticatedEncryption/Oracle.lean#L240 +[encryptionReal_bisim]: AuthenticatedEncryption/Oracle.lean#L369 +[hybrid_ideal_distance_le]: AuthenticatedEncryption/Collision.lean#L538 +[correctedChain]: AuthenticatedEncryption/Security.lean#L102 +[correctedChain_cca]: AuthenticatedEncryption/Security.lean#L121 +[correctedChain_ptxt]: AuthenticatedEncryption/Security.lean#L126 +[ae_of_ind_cca_int_ptxt]: AuthenticatedEncryption/Security.lean#L57 +[real_ideal_distance_le]: AuthenticatedEncryption/Security.lean#L132 +[advantage_attach_le_win]: Games.lean#L107 +[win_attach_le]: Games.lean#L54 +[win_attach_comp_le]: Games.lean#L68 +[win_le_of_reduction]: Games.lean#L87 +[collision]: Games.lean#L149 +[collision_visible]: Games.lean#L154 +[collision_conditionallyEquivalent]: Games.lean#L158 +[collision_win_le]: Games.lean#L165 +[hybrid_ideal_advantage_le]: Games.lean#L190 +[attach_hybrid_ideal_advantage_le]: Games.lean#L209 +[construction_with_right_context]: Substitution.lean#L43 +[construction_with_left_context]: Substitution.lean#L70 +[constructsWithin_of_two_substitutions]: Substitution.lean#L120 +[Padding]: DSL/Components.lean#L86 +[WriteThrough]: DSL/Components.lean#L104 +[FirstRequests]: DSL/Components.lean#L116 +[AES-system]: DSL/AES.lean#L29 +[CBC]: DSL/AES.lean#L57 +[EncryptThenMAC]: DSL/AEAD.lean#L47 diff --git a/src/Probability/README.md b/src/Probability/README.md new file mode 100644 index 0000000..c66ad32 --- /dev/null +++ b/src/Probability/README.md @@ -0,0 +1,80 @@ +# Probability + +This library holds the finitely supported laws on which the random systems are built: +distributions and probability distributions, kernels, the statistical distance, couplings and the +$`n`$-ary maximal coupling, expectation, and the counting behind collision bounds. Citations refer +to the numbered [references](../../THEORY.md#references) of THEORY.md. + +## Distributions and kernels + +*Finitely supported laws [1, Definitions 1–4]:* + +```math +\mathrm{Distribution}(A) = A \to_0 \mathbb R, \qquad +\delta(X, Y) = \sum_a \max\big(X(a) - Y(a),\ 0\big) . +``` + +A [**distribution**][Distribution] is a finitely supported function to $`\mathbb R`$, and a +[**probability distribution**][ProbDist] one that is [nonnegative with weight one][isProbDist]. +Distributions have [masses][mass] of events, [pushforwards][fTransform], [products][prod] of two +laws and of [families][pi], and [uniform][uniform] laws. A [**kernel**][bindK] $`f`$ is a conditional +distribution [3, §3.6.1]; mixed over a law $`\mu`$ it gives $`\sum_a \mu(a)\, f(a)`$: +[mixtures compose][bindK_bindK], a pushforward +[is the point kernel of its function][bindK_single_comp], and an independent product +[disintegrates][pi_eq_bindK_update] at a coordinate. Probability laws have +[pushforwards][ProbDist.map] and [sequential compositions][ProbDist.bind]. + +## Statistical distance + +The [**statistical distance**][statDist] +satisfies the [triangle inequality][statDist_triangle] and [data processing][statDist_fTransform_le], +$`\delta(fX, fY) \le \delta(X, Y)`$; with [positive parts][statDist_eq_weight_posPart] it is +$`\delta(X, Y) = \lvert (X - Y)^{+} \rvert`$, and with [overlaps][statDist_eq_weight_sub_weight_inf] +$`\delta(X, Y) = \lvert X \rvert - \lvert X \wedge Y \rvert`$. + +## Couplings, expectation and counting + +For a [coupling][IsCoupling] of $`X`$ and $`Y`$, +[the distance is at most the off-diagonal mass][statDist_le_offDiagonalMass], +$`\delta(X, Y) \le \Pr[X \ne Y]`$, and [some coupling attains it][exists_coupling_offDiagonalMass_eq]. +For the $`n`$-ary maximal coupling [2, Theorem 2.29], the [largest agreement][supAgreement] of $`n`$ +laws of one weight [is the weight of their overlap][supAgreement_eq_weight_overlapDist]. +[**Expectation**][expect] is linear [in the distribution][expect_add_left] and +[in the function][expect_add_right], with [Markov's][mass_ge_le_expect_div], +the [Cauchy–Schwarz][expect_mul_sq_le_sq_mul_sq] and [Jensen's][ConvexOn.map_expect_le] +inequalities. Collision bounds [count][card_function_fiber_finset] the functions $`X \to Y`$ +agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X \rvert - \lvert S \rvert}`$. + + + +[Distribution]: Distribution.lean#L56 +[ProbDist]: Distribution.lean#L149 +[isProbDist]: Distribution.lean#L128 +[mass]: Distribution.lean#L217 +[fTransform]: Distribution.lean#L632 +[prod]: Distribution.lean#L1005 +[pi]: Distribution.lean#L1646 +[uniform]: Distribution.lean#L566 +[bindK]: Kernel.lean#L49 +[bindK_bindK]: Kernel.lean#L95 +[bindK_single_comp]: Kernel.lean#L117 +[pi_eq_bindK_update]: Kernel.lean#L283 +[ProbDist.map]: Kernel.lean#L329 +[ProbDist.bind]: Kernel.lean#L341 +[statDist]: StatisticalDistance.lean#L88 +[statDist_triangle]: StatisticalDistance.lean#L243 +[statDist_fTransform_le]: StatisticalDistance.lean#L615 +[statDist_eq_weight_posPart]: Lift.lean#L89 +[statDist_eq_weight_sub_weight_inf]: Lift.lean#L170 +[IsCoupling]: Coupling.lean#L46 +[statDist_le_offDiagonalMass]: Coupling.lean#L241 +[exists_coupling_offDiagonalMass_eq]: Coupling.lean#L320 +[supAgreement]: MultiCoupling.lean#L87 +[supAgreement_eq_weight_overlapDist]: MultiCoupling.lean#L397 +[expect]: Expectation.lean#L44 +[expect_add_left]: Expectation.lean#L66 +[expect_add_right]: Expectation.lean#L96 +[mass_ge_le_expect_div]: Expectation.lean#L199 +[expect_mul_sq_le_sq_mul_sq]: Expectation.lean#L215 +[ConvexOn.map_expect_le]: Expectation.lean#L297 +[card_function_fiber_finset]: Counting.lean#L47 diff --git a/src/RandomSystems/Distance/README.md b/src/RandomSystems/Distance/README.md new file mode 100644 index 0000000..f319e36 --- /dev/null +++ b/src/RandomSystems/Distance/README.md @@ -0,0 +1,162 @@ +# Distance and distinguishers + +This folder holds the transcript distance of random systems and the ways to bound it: +probabilistic distinguishers and their behaviors, with the transcript distance as the largest +advantage; absorption of converters and systems into distinguishers; couplings; restriction to a +smaller domain; the H-coefficient bound; and the identical-until-bad bound. The systems, PDSs and +converters it uses are those of [RandomSystems](../README.md). Citations refer to the numbered +[references](../../../THEORY.md#references) of THEORY.md. + +## Distance and distinguishers + +The [**transcript distance**][RandomSystem.transcriptDistance] takes the supremum over environments +$`E`$ [compatible with the domain][Domain.Compatible] and [bounded][QueryBounded] to $`n`$ queries; a +[**probabilistic distinguisher**][Domain.Distinguisher] $`P`$ [1, Definition 9] has an +[advantage][Domain.Distinguisher.advantage]: + +```math +\Delta(R, S) = \sup_{E,\, n}\ \delta\big(\mathrm{tr}(R, E, n),\ \mathrm{tr}(S, E, n)\big), +\qquad +\mathrm{Adv}_P(R, S) = \big\lvert \Pr[P(R) = 1] - \Pr[P(S) = 1] \big\rvert . +``` + +A probabilistic distinguisher is a distribution over +[deterministic distinguishers][IsDDD] [compatible with the domain][Domain.DecisionCompatible], and its +[probability of outputting 1][Domain.Distinguisher.probability] averages their +[decision probabilities][RandomSystem.decisionProbability]. For each $`P`$, $`\mathrm{Adv}_P`$ is a +pseudo-distance: it is [zero on equal systems][advantage_self], [symmetric][advantage_symm], and +[satisfies the triangle inequality][advantage_triangle]. The transcript distance +[is the largest advantage][RandomSystem.transcriptDistance_eq_iSup], +$`\Delta(R, S) = \sup_P \mathrm{Adv}_P(R, S)`$, so +[every advantage is at most the distance][advantage_le_transcriptDistance]. + +The [**behavior**][Domain.DistinguisherBehavior] of a probabilistic distinguisher is its +probability of outputting 1 on each system, as the behavior of a PDC is its random system; the +transcript distance [is also the largest advantage of a behavior][RandomSystem.transcriptDistance_eq_iSup_behavior]. +A behavior has an [advantage][DistinguisherBehavior.advantage], which is +[zero on equal systems][DistinguisherBehavior.advantage_self], +[symmetric][DistinguisherBehavior.advantage_symm], satisfies the +[triangle inequality][DistinguisherBehavior.advantage_triangle], and +[is at most the distance][DistinguisherBehavior.advantage_le_transcriptDistance]. + +## Couplings + +The [transcript][System.tr] $`\mathrm{tr}(s, E, n)`$ of a deterministic system $`s`$ +with an environment $`E`$ within $`n`$ rounds is the sequence of their query–reply pairs +[1, Definition 7]. For an environment compatible with the random system $`R`$ of a PDS $`P`$, the +transcript law of $`R`$ [is the transformation][PDS.sLaw_behavior_eq_fTransform] of $`P`$ by +$`\mathrm{tr}(\cdot, E, n)`$ [1, Definition 4 and footnote 9]. A [coupling][IsCoupling] $`J`$ of +$`P`$ and a PDS $`Q`$ with random system $`S`$ therefore bounds the distance of the transcript laws +by the [probability that the transcripts differ][PDS.statDist_sLaw_behavior_le_of_isCoupling], and +the transcript distance by the +[probability that the systems differ][PDS.transcriptDistance_behavior_le_of_isCoupling]: + +```math +\delta\big(\mathrm{tr}(R, E, n),\ \mathrm{tr}(S, E, n)\big) +\le \Pr_{(s, t) \sim J}\big[\mathrm{tr}(s, E, n) \ne \mathrm{tr}(t, E, n)\big], +\qquad +\Delta(R, S) \le \Pr_{(s, t) \sim J}[s \ne t] . +``` + +The second bound holds for every coupling; [1, Theorem 2] states in addition that some +presentations of $`R`$ and $`S`$ have a coupling attaining it. + +## Absorption + +[Absorbing][DistinguisherBehavior.absorb] a PDC $`\alpha`$ into a behavior $`d`$ gives +$`d \circ \alpha`$, which decides on a system as $`d`$ decides on $`\alpha`$ attached to it, +$`\Pr[(d \circ \alpha)(R) = 1] = \Pr[d(\alpha R) = 1]`$. Absorbing a serial composition +[absorbs its PDCs in turn][DistinguisherBehavior.absorb_comp], +$`d \circ (\beta \circ \alpha) = (d \circ \beta) \circ \alpha`$. On deterministic distinguishers +absorption [connects the distinguisher to the converter's outside][absorbAll]; absorbing a +converter into a probabilistic distinguisher [gives a probabilistic distinguisher][Domain.Distinguisher.exists_absorbAll], +so $`d \circ \alpha`$ is a behavior, and so does absorbing +[a system run beside][Domain.Distinguisher.exists_absorbRight]. + +## Restriction + +The [restriction][RandomSystem.restrict] $`R \restriction D'`$ of a random system on $`D`$ +to a smaller domain $`D' \subseteq D`$ keeps the masses of the transcripts $`D'`$ admits and is zero +elsewhere. Restrictions [compose][RandomSystem.restrict_restrict], and an environment compatible +with $`D'`$ [sees the transcript law of the system itself][RandomSystem.sLaw_restrict], so restriction +[does not increase the distance][RandomSystem.transcriptDistance_restrict_le], +$`\Delta(R \restriction D', S \restriction D') \le \Delta(R, S)`$. + +## The H-coefficient bound + +Under an environment $`E`$, the transcript law of $`R`$ gives each +transcript $`h`$ that $`E`$ produces the probability $`R(h)`$, and the others zero; the restriction +is the same for $`S`$, so a ratio of the two systems' probabilities on the good transcripts is a +ratio of their transcript laws. For $`R`$ and $`S`$ replying at the queried label, the +H-coefficient technique then +[bounds the distance][RandomSystem.transcriptDistance_le_add_of_ratio_on_good] by the error +$`\varepsilon_1`$ of the ratio and the bound $`\varepsilon_2`$ on the bad transcripts under $`S`$: + +```math +(1 - \varepsilon_1)\, S(h) \le R(h) \ \text{ for } h \notin \mathrm{Bad}, \quad +\Pr_{\mathrm{tr}(S, E, n)}[\mathrm{Bad}] \le \varepsilon_2 \ \text{ for all } E, n +\quad \Longrightarrow \quad +\Delta(R, S) \le \varepsilon_1 + \varepsilon_2 . +``` + +## Identical until bad + +Two random systems $`R_1`$ and $`R_2`$ have transcript probabilities that both lie above a common +part $`g`$ with $`g([]) = 1`$. A step from a possible transcript $`h`$ by an admitted query $`x`$ +loses $`g(h) - \sum_y g(h, x, y)`$ of the common part. If each step loses at most +$`\beta(h, x)\, R_1(h)`$, and the [cost][transcriptCost] of each possible transcript, the sum of +$`\beta`$ over its steps, is at most $`\varepsilon`$, then by the union bound over the steps every +compatible environment [stays in the common part][RandomSystem.one_sub_le_sum_tSupp] with +probability at least $`1 - \varepsilon`$, and the two systems are +[within][RandomSystem.transcriptDistance_le_of_transcriptCost_le] $`\varepsilon`$ of each other: + +```math +g(h) - \sum_y g(h, x, y) \le \beta(h, x)\, R_1(h), \qquad +\sum_{k < |h|} \beta(h_1 \cdots h_k,\ x_{k+1}) \le \varepsilon +\quad \Longrightarrow \quad +\Delta(R_1, R_2) \le \varepsilon . +``` + +Games build on this bound: see [Game](../Game/README.md#identical-until-bad). + + + +[RandomSystem.transcriptDistance]: Decision.lean#L228 +[Domain.Compatible]: Decision.lean#L165 +[Domain.DecisionCompatible]: Decision.lean#L171 +[QueryBounded]: ../System/DDE.lean#L24 +[IsDDD]: ../System/InterfaceSystem.lean#L968 +[RandomSystem.decisionProbability]: Decision.lean#L262 +[Domain.Distinguisher]: Distinguisher.lean#L122 +[Domain.Distinguisher.probability]: Distinguisher.lean#L126 +[Domain.Distinguisher.advantage]: Distinguisher.lean#L132 +[advantage_self]: Distinguisher.lean#L141 +[advantage_symm]: Distinguisher.lean#L143 +[advantage_triangle]: Distinguisher.lean#L146 +[RandomSystem.transcriptDistance_eq_iSup]: Distinguisher.lean#L154 +[advantage_le_transcriptDistance]: Distinguisher.lean#L196 +[Domain.DistinguisherBehavior]: Distinguisher.lean#L207 +[DistinguisherBehavior.advantage]: Distinguisher.lean#L218 +[DistinguisherBehavior.advantage_self]: Distinguisher.lean#L228 +[DistinguisherBehavior.advantage_symm]: Distinguisher.lean#L230 +[DistinguisherBehavior.advantage_triangle]: Distinguisher.lean#L233 +[DistinguisherBehavior.advantage_le_transcriptDistance]: Distinguisher.lean#L238 +[RandomSystem.transcriptDistance_eq_iSup_behavior]: Distinguisher.lean#L246 +[System.tr]: Coupling.lean#L50 +[IsCoupling]: ../../Probability/Coupling.lean#L46 +[PDS.sLaw_behavior_eq_fTransform]: Coupling.lean#L165 +[PDS.statDist_sLaw_behavior_le_of_isCoupling]: Coupling.lean#L213 +[PDS.transcriptDistance_behavior_le_of_isCoupling]: Coupling.lean#L241 +[DistinguisherBehavior.absorb]: Distinguisher.lean#L291 +[DistinguisherBehavior.absorb_comp]: Distinguisher.lean#L304 +[Domain.Distinguisher.exists_absorbAll]: Distinguisher.lean#L265 +[Domain.Distinguisher.exists_absorbRight]: Distinguisher.lean#L330 +[absorbAll]: Absorption.lean#L42 +[RandomSystem.restrict]: Restriction.lean#L59 +[RandomSystem.restrict_restrict]: Restriction.lean#L67 +[RandomSystem.sLaw_restrict]: Restriction.lean#L98 +[RandomSystem.transcriptDistance_restrict_le]: Restriction.lean#L129 +[RandomSystem.transcriptDistance_le_add_of_ratio_on_good]: HCoefficient.lean#L40 +[transcriptCost]: UntilBad.lean#L38 +[RandomSystem.one_sub_le_sum_tSupp]: UntilBad.lean#L65 +[RandomSystem.transcriptDistance_le_of_transcriptCost_le]: UntilBad.lean#L146 diff --git a/src/RandomSystems/Game/README.md b/src/RandomSystems/Game/README.md new file mode 100644 index 0000000..40c49b8 --- /dev/null +++ b/src/RandomSystems/Game/README.md @@ -0,0 +1,154 @@ +# 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](../README.md) and [Distance](../Distance/README.md). Citations refer to +the numbered [references](../../../THEORY.md#references) of THEORY.md. + +## Games, winning and conditional equivalence + +A [**game**][RandomSystem.MonotoneMBO] is a random system whose replies carry a bit, the MBO, +which once set stays set [3, §3.7.1]. Its [**visible system**][RandomSystem.visible] $`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][DDE.blindMBO], and its +[**winning probability**][RandomSystem.winProbability] is the probability that the MBO is set when +it stops [3, Definition 4.5]. A game is [**conditionally equivalent**][RandomSystem.ConditionallyEquivalent] +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][Domain.Distinguisher.advantage_le_winProbability] +[3, Lemma 4.16 and the proof of Theorem 4.17]: + +```math +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][Domain.Distinguisher.winProbability_le_of_unsetProbability] $`\varepsilon`$. +The transcript distance is the largest advantage ([Distance](../Distance/README.md)), so the +visible system is then +[within][RandomSystem.transcriptDistance_visible_le_of_unsetProbability] $`\varepsilon`$ of $`T`$ +[3, Theorem 4.17], [5, Theorem 3], for $`G`$ and $`T`$ replying at the queried label: + +```math +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**][RandomSystem.GameEquivalent], $`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][Domain.Distinguisher.winProbability_eq_of_gameEquivalent] [3, Lemma 4.15], and +by the fundamental lemma its advantage between their visible systems is +[at most its winning probability][Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent] +[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: + +```math +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](../Distance/README.md#identical-until-bad): 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][Domain.Distinguisher.winProbability_le_of_transcriptCost_le] +$`\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][RandomSystem.GameEquivalent.transcriptDistance_visible_le] $`\varepsilon`$ of +each other. Two discrete games are equivalent as games when they are +[coupled][PDG.gameEquivalent_behavior_of_isCoupling]: 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][PDCBehavior.liftMBO] $`\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][PDCBehavior.liftMBO_id], $`\hat{\mathrm{id}} = \mathrm{id}`$, and +[composition][PDCBehavior.liftMBO_comp], $`\widehat{\alpha \beta} = \hat\alpha \hat\beta`$. It +[keeps games games][RandomSystem.MonotoneMBO.attach_liftMBO] and +[commutes with the visible system][RandomSystem.visible_attach_liftMBO], +$`(\hat\alpha G)^- = \alpha\, G^-`$. A winner with $`\alpha`$ absorbed +wins $`G`$ [as the winner wins][RandomSystem.winProbability_attach_liftMBO] $`\hat\alpha G`$ +[3, §4.7.2, equation (4.9)]. A [**solver behavior**][Domain.SolverBehavior] pairs a probabilistic +distinguisher's probability of outputting 1 on each random system with its winning probability +for each game, and [absorbing a PDC][Domain.SolverBehavior.absorb] into a solver behavior gives a +solver behavior. + +## Discrete games + +Discrete games present games, as PDSs present random systems. A [discrete game][PDG] is a +distribution over [deterministic discrete games][DDG], pairs of a DDS and a hidden +[monotone condition][MC] 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][DDG.withMBO] as its MBO, +and a discrete game [presents the game][PDG.behavior] of these systems. Its visible system +[is the behavior of the visible systems][PDG.visible_behavior], and on an admitted query sequence +the MBO [is unset with the probability that the condition does not hold][PDG.unsetProbability_behavior], +so a bound on the condition at the empty and every admitted query sequence +[bounds the probability that the MBO is set][PDG.one_sub_le_unsetProbability_behavior]. The game +is [conditionally equivalent][PDG.conditionallyEquivalent_behavior] to a random system $`S`$ when +the replies with the condition unset factor through $`S`$: + +```math +\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][PDG.ofFunction] is a discrete game, and the game it +presents is [conditionally equivalent to the ideal function][PDG.ofFunction_conditionallyEquivalent] +once, on every fixed query sequence, the answers jointly with the unset condition factor through +the ideal answers. + + + +[RandomSystem.MonotoneMBO]: MBO.lean#L305 +[RandomSystem.visible]: MBO.lean#L340 +[DDE.blindMBO]: MBO.lean#L410 +[RandomSystem.winProbability]: MBO.lean#L480 +[RandomSystem.ConditionallyEquivalent]: MBO.lean#L523 +[RandomSystem.GameEquivalent]: MBO.lean#L537 +[Domain.Distinguisher.advantage_le_winProbability]: MBO.lean#L756 +[Domain.Distinguisher.winProbability_eq_of_gameEquivalent]: MBO.lean#L860 +[Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent]: MBO.lean#L874 +[Domain.Distinguisher.winProbability_le_of_unsetProbability]: MBO.lean#L951 +[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: MBO.lean#L976 +[Domain.Distinguisher.winProbability_le_of_transcriptCost_le]: UntilBad.lean#L148 +[RandomSystem.GameEquivalent.transcriptDistance_visible_le]: UntilBad.lean#L177 +[PDG.gameEquivalent_behavior_of_isCoupling]: UntilBad.lean#L209 +[PDCBehavior.liftMBO]: MBOAttachment.lean#L455 +[PDCBehavior.liftMBO_id]: MBOAttachment.lean#L495 +[PDCBehavior.liftMBO_comp]: MBOAttachment.lean#L1515 +[RandomSystem.MonotoneMBO.attach_liftMBO]: MBOAttachment.lean#L965 +[RandomSystem.visible_attach_liftMBO]: MBOAttachment.lean#L619 +[RandomSystem.winProbability_attach_liftMBO]: MBOAttachment.lean#L2079 +[Domain.SolverBehavior]: MBOAttachment.lean#L2169 +[Domain.SolverBehavior.absorb]: MBOAttachment.lean#L2191 +[MC]: DiscreteMBO.lean#L46 +[DDG]: DiscreteMBO.lean#L50 +[PDG]: DiscreteMBO.lean#L54 +[DDG.withMBO]: DiscreteMBO.lean#L103 +[PDG.behavior]: DiscreteMBO.lean#L235 +[PDG.visible_behavior]: DiscreteMBO.lean#L253 +[PDG.unsetProbability_behavior]: DiscreteMBO.lean#L331 +[PDG.one_sub_le_unsetProbability_behavior]: DiscreteMBO.lean#L434 +[PDG.conditionallyEquivalent_behavior]: DiscreteMBO.lean#L460 +[PDG.ofFunction]: FunctionGame.lean#L37 +[PDG.ofFunction_conditionallyEquivalent]: FunctionGame.lean#L73 diff --git a/src/RandomSystems/README.md b/src/RandomSystems/README.md new file mode 100644 index 0000000..83d18b5 --- /dev/null +++ b/src/RandomSystems/README.md @@ -0,0 +1,207 @@ +# Random systems + +This library holds the concrete objects and their laws: deterministic systems, automata and +environments (`System`), distributions over deterministic systems (`PDS`), random systems given by +their cumulative probabilities, with their presentations (`Cumulative`), deterministic converters +and their compositions (`DDC`), probabilistic converters, programs, attachment and parallel +composition (`Converter`), the transcript distance and distinguishers +([`Distance`](Distance/README.md)), games ([`Game`](Game/README.md)), and typed systems on +interfaces ([`Typed`](Typed/README.md)). It knows nothing of the classes of +[ConstructiveCryptography](../ConstructiveCryptography/README.md), whose instances on interfaces +take their fields from here. Citations refer to the numbered +[references](../../THEORY.md#references) of THEORY.md. + +*Systems over finite alphabets, answering exactly on a bounded domain [1], [2, Chapter 2], +[3, Chapter 3]. Laws are finitely supported distributions and $`\delta`$ is the statistical +distance ([Probability](../Probability/README.md)).* + +## Deterministic systems + +A [**deterministic system**][IsDDS] (DDS) is a [partial function][System] from input histories to +the next output, $`s : \mathcal X^{*} \rightharpoonup \mathcal Y`$, [silent at the empty +history][SilentAtEmpty], whose domain is [closed under nonempty prefixes][PrefixClosed]. Systems +are [wired together][interconnect], each output leaving the wiring or returning as an input. A +system [replies][Replies] $`y_1 \dots y_n`$ to $`x_1 \dots x_n`$ when it answers each prefix with the +next output, and a DDS [is determined by its completed replies][IsDDS.eq_of_replies_iff]. An +[automaton][automatonSystem] is a transition function started in a state, and +[bisimilar][IsBisim] automata [have the same system][automatonSystem_eq_of_bisim]. An +[environment][DDE] (DDE) chooses the next query from the replies so far. + +## Probabilistic systems + +A [**domain**][Domain] $`\mathcal D`$ admits next queries after each transcript, with a bound on the +length. A [**PDS**][PDS] is a finite distribution over DDSs [with domain][HasDomain] +$`\mathcal D`$ [1, Definition 8]. A [**random system**][RandomSystem] is given by its cumulative +probabilities $`p`$ on transcripts [1, after Lemma 5], [normalized][IsRandomSystem] on the domain: + +```math +p(\varepsilon) = 1, \qquad p \ge 0, \qquad +\sum_{y} p\big(h \cdot (x, y)\big) = +\begin{cases} p(h) & \text{if } x \text{ is admitted after } h, \\ 0 & \text{otherwise.} \end{cases} +``` + +A PDS [has a random system][PDS.behavior], and [equivalent][Equivalent] PDSs +[have the same one][PDS.behavior_eq_iff]. Every random system +[has a finite presentation][RandomSystem.exists_presentation], so random systems +[are exactly the classes of equivalent PDSs][RandomSystem.ofPDSClass_bijective]. Two random +systems [are equal exactly when][RandomSystem.eq_iff_sLaw] their +[transcript laws][RandomSystem.sLaw] agree in every [compatible][RandomSystem.Compatible] +environment, and on a domain of input histories +[fixed query sequences suffice][RandomSystem.eq_iff_sLaw_fixedQueries] [1, Lemma 5]. Random +systems on one domain form [mixtures][RandomSystem.mix], and two random systems run +[independently in parallel][RandomSystem.parallel] form one on the combined alphabets. + +A [**probabilistic automaton**][RandomSystem.ofProbAutomaton] answers a query from its state with a +law on the next state and the reply, a [probabilistic step][ProbStep]; its random system follows +the [sub-law of the states][ProbStep.belief] reached with the replies of a transcript, whose weight +is the probability of the transcript. On an input domain, two probabilistic automata +[have the same random system][RandomSystem.ofProbAutomaton_eq_of_simulation] along a +[simulation][ProbStep.SimulatesAt], a kernel between their states through which their steps +commute. A deterministic automaton with a random initial state +[is the probabilistic automaton of its point steps][RandomSystem.ofProbAutomaton_ofDeterministic_apply], +and a probabilistic automaton +[is a deterministic automaton reading pre-sampled draws][RandomSystem.ofProbAutomaton_eq_drawStep], +sampled once with the initial state: a random automaton [4, Definition 2]. + +A random system is [**memoryless**][RandomSystem.memoryless] when the law of its reply depends only +on the current query, never on the history: a source "can be memoryless or have memory" +[3, Definition 3.1], and a single-input system given by a conditional distribution is a "discrete +memoryless channel" [3, §3.6.1]. With the reply law $`\nu`$, its probabilities obey the chain rule + +```math +p\big(h \cdot (x, y)\big) = p(h)\, \nu_x(y) \qquad \text{for every query } x \text{ admitted after } h, +``` + +and [a random system obeying it is the memoryless system][RandomSystem.eq_memoryless_of_snoc]. +A probabilistic automaton whose step [replies from every state with the same +law][ProbStep.Memoryless] $`\nu`$ [is the memoryless system of this law][RandomSystem.ofProbAutomaton_eq_memoryless]. +Two memoryless systems [side by side are memoryless][RandomSystem.parallel_memoryless]: a query +to either system is answered with the reply law of that system. + +## Converters + +A [**DDC**][IsDDC] is a system on the converter alphabets (outside queries and inside replies in; +inside queries and outside replies out) with at most $`b`$ consecutive inside queries +[3, Definition 3.8]. A **DDC from $`E`$ to $`F`$** ([`IsDDCFrom`][IsDDCFrom]) answers exactly the +[converter domain][converterDomain] and queries only in $`E`$; attached to a system with domain $`E`$ +it [gives one with domain][IsDDCFrom.mapsDomain] $`F`$. A [**PDC**][PDCBehavior.ofPDC] is a distribution over DDCs, and +its [**behavior**][PDCBehavior] is a random system over the converter domain +[3, Definitions 3.17–3.18]. + +[Serial composition][serialM] $`\beta \odot \alpha`$ connects the inside of $`\beta`$ to the outside +of $`\alpha`$, and [DDCs compose][IsDDC.comp] with the product of their bounds. PDC behaviors have a +[composition][PDCBehavior.comp] and an [identity][PDCBehavior.id], with +[associativity][PDCBehavior.comp_assoc] and the [left][PDCBehavior.id_comp] and +[right][PDCBehavior.comp_id] identity laws. [Attachment][PDCBehavior.attach] samples the PDC, then +attaches the sample deterministically: [presentations attach to +presentations][PDCBehavior.attach_presents], [the identity leaves a system +unchanged][PDCBehavior.attach_id], and [a composition attaches its inner converter +first][PDCBehavior.attach_comp]. [Parallel composition][PDCBehavior.tensor] samples two PDCs +independently and runs them side by side, with [interchange][PDCBehavior.comp_tensor] against +serial composition. + +A [**program**][Program] is a deterministic oracle body: from its state, the outside query and the +inside exchanges of the current invocation, it computes the reply or the next inside query. A +program can be [bounded][Program.Bounded] (at most $`b`$ inside queries per invocation), have +[exact costs][Program.Costs], or [preserve a partial port map][Program.PortPreserving] +$`\iota : O \to \mathrm{Option}\ J`$: an invocation at $`o`$ queries the labels in the image of +$`\iota`$ only at $`\iota(o)`$, at most once, and none of them when $`\iota(o)`$ is none, so it +queries $`\iota(o)`$ [at most as often as it is queried at][DDC.insideQueries_restrict_length_le] +$`o`$. On an outside domain, a bounded program +[is a DDC from every inside domain containing its inside queries][DDC.ofProgramOn_isDDCFrom]. +Attached to an automaton, a program is [inlined][Program.inline] [4, §3.3]: the result is the +[combined automaton][Program.combine] on pairs of states, also +[on domains][Program.trim_apply_ofProgramOn_automaton]. + +Run against a probabilistic automaton, a program is the probabilistic automaton +[on pairs of states][Program.probCombine] whose step runs one invocation, the automaton answering +the inside queries with fresh steps; it [respects simulations][RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation]. +[**Attaching the program's converter to a probabilistic automaton is the program run against +it**][PDCBehavior.attach_ofDDC_ofProgramOn_ofProbAutomaton], the combined system $`C(F)`$ of a +system $`C(\cdot)`$ invoking $`F`$ [4, §3.3]; for point steps it is the +[combined automaton][PDCBehavior.attach_ofDDC_ofProgramOn_ofDeterministic]. Against memoryless +replies of the laws $`\nu`$, a program [replies memorylessly][Program.memoryless_probCombine] when +its [reply law][Program.replyLaw] $`\kappa`$, the law of one invocation whose inside queries are +answered by fresh samples of $`\nu`$, is the same from every program state. So [the composition law][PDCBehavior.attach_ofDDC_ofProgramOn_memoryless] +holds, whatever the number of the program's inside queries: + +```math +\alpha_P\, \mathrm{mem}(\nu) = \mathrm{mem}(\kappa). +``` + + + +[System]: System/Basic.lean#L40 +[SilentAtEmpty]: System/Basic.lean#L69 +[PrefixClosed]: System/Basic.lean#L72 +[IsDDS]: System/Basic.lean#L77 +[interconnect]: System/Basic.lean#L225 +[Replies]: System/Replies.lean#L33 +[IsDDS.eq_of_replies_iff]: System/Replies.lean#L151 +[automatonSystem]: System/Automaton.lean#L43 +[IsBisim]: System/Automaton.lean#L70 +[automatonSystem_eq_of_bisim]: System/Automaton.lean#L89 +[DDE]: System/DDE.lean#L20 +[Domain]: PDS/PDS.lean#L65 +[Equivalent]: PDS/PDS.lean#L50 +[HasDomain]: PDS/PDS.lean#L91 +[PDS]: PDS/PDS.lean#L133 +[IsRandomSystem]: Cumulative/Cumulative.lean#L39 +[RandomSystem]: Cumulative/Cumulative.lean#L53 +[PDS.behavior]: Cumulative/Cumulative.lean#L216 +[PDS.behavior_eq_iff]: Cumulative/Cumulative.lean#L225 +[RandomSystem.exists_presentation]: Cumulative/Presentation.lean#L302 +[RandomSystem.ofPDSClass_bijective]: Cumulative/Presentation.lean#L312 +[RandomSystem.sLaw]: Cumulative/CumulativeObservation.lean#L179 +[RandomSystem.Compatible]: Cumulative/CumulativeObservation.lean#L197 +[RandomSystem.eq_iff_sLaw]: Cumulative/CumulativeObservation.lean#L534 +[RandomSystem.eq_iff_sLaw_fixedQueries]: Cumulative/CumulativeObservation.lean#L548 +[RandomSystem.mix]: Cumulative/CumulativeOperations.lean#L45 +[RandomSystem.parallel]: Cumulative/CumulativeOperations.lean#L130 +[RandomSystem.ofProbAutomaton]: System/ProbAutomaton.lean#L197 +[ProbStep]: System/ProbAutomaton.lean#L58 +[ProbStep.belief]: System/ProbAutomaton.lean#L160 +[ProbStep.SimulatesAt]: System/ProbAutomaton.lean#L260 +[RandomSystem.ofProbAutomaton_eq_of_simulation]: System/ProbAutomaton.lean#L400 +[RandomSystem.ofProbAutomaton_ofDeterministic_apply]: System/ProbAutomaton.lean#L535 +[RandomSystem.ofProbAutomaton_eq_drawStep]: Converter/ProbProgramAttachment.lean#L933 +[RandomSystem.memoryless]: System/Memoryless.lean#L65 +[RandomSystem.eq_memoryless_of_snoc]: System/Memoryless.lean#L84 +[RandomSystem.parallel_memoryless]: System/Memoryless.lean#L146 +[ProbStep.Memoryless]: System/Memoryless.lean#L237 +[RandomSystem.ofProbAutomaton_eq_memoryless]: System/Memoryless.lean#L273 +[IsDDC]: DDC/DDC.lean#L127 +[serialM]: DDC/Serial.lean#L55 +[IsDDC.comp]: DDC/Serial.lean#L514 +[converterDomain]: Converter/ConverterDomain.lean#L234 +[IsDDCFrom]: Converter/ConverterDomain.lean#L301 +[IsDDCFrom.mapsDomain]: Converter/ConverterDomain.lean#L609 +[PDCBehavior]: Converter/PDCBehavior.lean#L67 +[PDCBehavior.ofPDC]: Converter/PDCBehavior.lean#L169 +[PDCBehavior.comp]: Converter/PDCBehavior.lean#L273 +[PDCBehavior.id]: Converter/PDCBehavior.lean#L369 +[PDCBehavior.comp_assoc]: Converter/PDCBehavior.lean#L338 +[PDCBehavior.id_comp]: Converter/PDCBehavior.lean#L385 +[PDCBehavior.comp_id]: Converter/PDCBehavior.lean#L375 +[PDCBehavior.attach]: Converter/ConverterAttachment.lean#L156 +[PDCBehavior.attach_presents]: Converter/ConverterAttachment.lean#L178 +[PDCBehavior.attach_id]: Converter/ConverterAttachment.lean#L233 +[PDCBehavior.attach_comp]: Converter/ConverterAttachment.lean#L246 +[PDCBehavior.tensor]: Converter/ConverterTensor.lean#L649 +[PDCBehavior.comp_tensor]: Converter/ConverterTensor.lean#L745 +[Program]: Converter/Program.lean#L45 +[Program.Bounded]: Converter/Program.lean#L70 +[Program.Costs]: Converter/Program.lean#L112 +[Program.PortPreserving]: Converter/Program.lean#L123 +[DDC.insideQueries_restrict_length_le]: Converter/Program.lean#L537 +[DDC.ofProgramOn_isDDCFrom]: Converter/Program.lean#L634 +[Program.inline]: Converter/ProgramAttachment.lean#L258 +[Program.combine]: Converter/ProgramAttachment.lean#L429 +[Program.trim_apply_ofProgramOn_automaton]: Converter/ProgramAttachment.lean#L609 +[Program.probCombine]: Converter/ProbProgramAttachment.lean#L187 +[RandomSystem.ofProbAutomaton_probCombine_eq_of_simulation]: Converter/ProbProgramAttachment.lean#L507 +[PDCBehavior.attach_ofDDC_ofProgramOn_ofProbAutomaton]: Converter/ProbProgramAttachment.lean#L1095 +[PDCBehavior.attach_ofDDC_ofProgramOn_ofDeterministic]: Converter/ProbProgramAttachment.lean#L1009 +[Program.replyLaw]: System/Memoryless.lean#L304 +[Program.memoryless_probCombine]: System/Memoryless.lean#L390 +[PDCBehavior.attach_ofDDC_ofProgramOn_memoryless]: System/Memoryless.lean#L421 diff --git a/src/RandomSystems/Typed/README.md b/src/RandomSystems/Typed/README.md new file mode 100644 index 0000000..bacc64d --- /dev/null +++ b/src/RandomSystems/Typed/README.md @@ -0,0 +1,158 @@ +# Typed systems + +This folder holds the random systems and converters of [RandomSystems](../README.md), typed by +interfaces [3, Definitions 3.8, 3.9, 3.17], [6, §3], [7, Definitions 2.2.1–2.2.2]: interfaces and +their budgets, typed systems and typed converters, attachment, parallel composition and renaming +with their coherence laws, filters, contexts, sources, automata, memoryless and functional +systems, typed games and the typed games presented by discrete games. Its `DSL` folder holds the +part of the DSL below the front end: the surface syntax, the laws that components sample from, +program bodies and their typed converters, and the tactics for the generated obligations +([GRAMMAR](../../ConstructiveCryptography/DSL/GRAMMAR.md)). +Every object here is a systems-level object; the instances of the classes in +[ConstructiveCryptography](../../ConstructiveCryptography/README.md) use them as their fields. +Citations refer to the numbered [references](../../../THEORY.md#references) of THEORY.md. + +## Interfaces, typed systems and typed converters + +An [**interface**][Interface] $`A = (I, X, Y, D)`$ has finitely many labels, finite alphabets +$`X_i, Y_i`$, and a domain $`D`$ of input histories, prefix-closed, without the empty history, of +bounded length. Two domains recur: the [**query budget**][Interface.queryBudget] +$`D = \lbrace h \ne \varepsilon \mid \lvert h \rvert \le q \rbrace`$ and the +[**per-port budget**][Interface.portBudget] +$`D = \lbrace h \ne \varepsilon \mid \forall i.\ \lvert h \restriction i \rvert \le q_i \rbrace`$, +where $`h \restriction i`$ [keeps the inputs at the label][restrict] $`i`$. + +A [**typed system**][TypedSystem] on $`A`$ is a random system on +$`(\Sigma_i X_i, \Sigma_i Y_i)`$ over $`D`$, +[replying at the queried label][RandomSystem.RepliesAtQueriedInterface]. A +[**typed converter**][TypedConverter] from $`A`$ to $`B`$ is a PDC behavior from $`B`$'s domain +(inside) to $`A`$'s domain (outside), and a DDC between the two domains +[is one][TypedConverter.ofDDC]. Typed converters compose by the [serial composition][TypedConverter.comp] +of PDC behaviors, with the [identity][TypedConverter.id] PDC behavior. +[**Attachment**][TypedConverter.attach] $`\alpha R`$ is the attachment of the PDC behavior: +[the identity leaves a typed system unchanged][TypedConverter.identity_attach], and +[a serial composition attaches its inner converter first][TypedConverter.comp_smul]. + +[**Parallel interfaces**][Interface.tensor] put the label sets side by side, and +[parallel typed systems][TypedSystem.parallel] and [parallel typed converters][TypedConverter.parallel] +are the independent parallel compositions; attachment [is local][TypedConverter.parallel_attach], +$`(\alpha \otimes \beta)(R \parallel S) = \alpha R \parallel \beta S`$. A label-preserving +bijection of interfaces gives a [**renaming**][TypedConverter.rename], which +[relabels the transcripts][TypedConverter.rename_mass] of the typed system it is attached to; +renamings [compose][TypedConverter.rename_comp], and the renaming by the identity +[is the identity][TypedConverter.rename_refl]. Regrouping three parallel typed systems +[keeps the probabilities][TypedSystem.parallel_assoc_mass] of the regrouped transcripts, the +[dummy system][TypedSystem.dummy] on the [interface without labels][Interface.unit] beside a typed +system keeps its probabilities, on the [left][TypedSystem.parallel_unit_left_mass] and on the +[right][TypedSystem.parallel_unit_right_mass], and [exchanging the two components][TypedSystem.parallel_swap_mass] +of a parallel composition exchanges the labels of its transcripts. The regrouping renamings are +natural for typed converters: [associativity][TypedConverter.comp_associator] and the +[left][TypedConverter.comp_leftUnitor] and [right][TypedConverter.comp_rightUnitor] unit +regroupings commute with parallel typed converters, and the parallel composition of two renamings +[is the renaming of their union][TypedConverter.parallel_rename]. + +## Filters, contexts, sources and functional systems + +The [**filter**][TypedConverter.filter] admitting $`D`$ forwards the queries of admitted histories; +it is a typed converter $`(A \restriction D) \to A`$ from the [restricted interface][Interface.restrict]. +[Attached to a typed system][TypedConverter.filter_smul], it is the +[restriction][RandomSystem.restrict] of the system's random system to the restricted domain, and +[two filters in series][TypedConverter.filter_comp_filter_smul] act as the filter of both +conditions. A [**constant**][TypedConverter.constant] converter ignores its inside system and +exposes a fixed one, and the fixed [right][TypedConverter.rightContext] and +[left][TypedConverter.leftContext] **contexts** run a typed system beside: +[attaching][TypedConverter.attach_rightContext] $`\mathrm{rightContext}\ A\ S`$ to $`R`$ +gives $`R \parallel S`$, and so does [attaching][TypedConverter.attach_leftContext] +$`\mathrm{leftContext}\ R\ B`$ to $`S`$. + +A [**source**][TypedSystem.source] answers with fresh independent samples of a law: a +memoryless source [3, Definition 3.1] (the sources of [4, Definition 1] may have memory). An +[**automaton**][TypedSystem.ofAutomaton] is a transition function with a sampled initial state +[4, Definition 2], and [parallel automata][TypedSystem.parallel_ofAutomaton] are the automaton +running both side by side. A source [is memoryless][TypedSystem.source_eq_memoryless], +memoryless systems [side by side are memoryless][TypedSystem.parallel_eq_memoryless], and the +converter of a program [maps a memoryless system to the memoryless system of its reply +law][TypedConverter.ofProgram_smul_memoryless], also +[for port-preserving programs][TypedConverter.ofPreservingProgram_smul_memoryless] and +[with its own sources beside its inside interface][TypedConverter.ofPreservingProgram_comp_rightContext_smul_memoryless]: +the composition law of [converters](../README.md#converters) on their random systems. +**Functional systems** are given by [reply functions][TypedSystem.ofFunction], by +[conditional reply laws][TypedSystem.ofConditional], or by +[sampling once][TypedSystem.sample] and keeping the sample. + +## Typed games + +A [**typed game**][TypedGame] on $`A`$ is a typed system on the [interface][Interface.withMBO] of +$`A`$ with the MBO whose MBO, once set, stays set: a game in the sense of +[Game](../Game/README.md). A typed converter [attaches][TypedConverter.attachGame] to it through its +[MBO-forwarding lift][PDCBehavior.liftMBO], and its [visible typed system][TypedGame.visible] is its +visible system. A discrete game whose visible systems present a typed system $`R`$ +[presents a typed game][TypedGame.ofPDG] on the interface of $`R`$, with +[visible typed system][TypedGame.visible_ofPDG] $`R`$. A single-label sampled function with a +hidden condition [presents a typed game][TypedGame.ofSingleFunction] whose random system is +[conditionally equivalent][TypedGame.ofSingleFunction_conditionallyEquivalent] to that of the +typed system sampling the ideal function, under the fixed-query factorization. + + + +[Interface]: Interface.lean#L40 +[Interface.queryBudget]: Interface.lean#L63 +[Interface.portBudget]: Interface.lean#L74 +[restrict]: ../System/Basic.lean#L794 +[TypedSystem]: Interface.lean#L92 +[RandomSystem.RepliesAtQueriedInterface]: ../Cumulative/Cumulative.lean#L70 +[TypedConverter]: Interface.lean#L127 +[TypedConverter.ofDDC]: Interface.lean#L143 +[TypedConverter.comp]: Interface.lean#L134 +[TypedConverter.id]: Interface.lean#L139 +[TypedConverter.attach]: Interface.lean#L157 +[TypedConverter.identity_attach]: Interface.lean#L171 +[TypedConverter.comp_smul]: Interface.lean#L177 +[Interface.tensor]: Parallel.lean#L85 +[TypedSystem.parallel]: Parallel.lean#L153 +[TypedConverter.parallel]: Parallel.lean#L210 +[TypedConverter.parallel_attach]: ParallelAttachment.lean#L23 +[TypedConverter.rename]: Relabel.lean#L48 +[TypedConverter.rename_comp]: Relabel.lean#L80 +[TypedConverter.rename_refl]: Relabel.lean#L67 +[TypedConverter.rename_mass]: SystemParallel.lean#L55 +[TypedSystem.parallel_assoc_mass]: SystemCoherence.lean#L85 +[TypedSystem.dummy]: SystemCoherence.lean#L97 +[Interface.unit]: InterfaceCoherence.lean#L90 +[TypedSystem.parallel_unit_left_mass]: SystemCoherence.lean#L103 +[TypedSystem.parallel_unit_right_mass]: SystemCoherence.lean#L128 +[TypedSystem.parallel_swap_mass]: SystemCoherence.lean#L153 +[TypedConverter.comp_associator]: ConverterCoherence.lean#L158 +[TypedConverter.comp_leftUnitor]: ConverterCoherence.lean#L195 +[TypedConverter.comp_rightUnitor]: ConverterCoherence.lean#L224 +[TypedConverter.parallel_rename]: TensorRename.lean#L128 +[Interface.restrict]: Filter.lean#L32 +[TypedConverter.filter]: Filter.lean#L49 +[TypedConverter.filter_smul]: Filter.lean#L60 +[TypedConverter.filter_comp_filter_smul]: Filter.lean#L94 +[RandomSystem.restrict]: ../Distance/Restriction.lean#L59 +[TypedConverter.constant]: Context.lean#L78 +[TypedConverter.rightContext]: Context.lean#L109 +[TypedConverter.leftContext]: Context.lean#L116 +[TypedConverter.attach_rightContext]: Context.lean#L122 +[TypedConverter.attach_leftContext]: Context.lean#L127 +[TypedSystem.source]: Source.lean#L51 +[TypedSystem.ofAutomaton]: Automaton.lean#L42 +[TypedSystem.parallel_ofAutomaton]: Automaton.lean#L57 +[TypedSystem.source_eq_memoryless]: Memoryless.lean#L47 +[TypedSystem.parallel_eq_memoryless]: Memoryless.lean#L146 +[TypedConverter.ofProgram_smul_memoryless]: Memoryless.lean#L241 +[TypedConverter.ofPreservingProgram_smul_memoryless]: Memoryless.lean#L262 +[TypedConverter.ofPreservingProgram_comp_rightContext_smul_memoryless]: Memoryless.lean#L279 +[TypedSystem.ofFunction]: Functional.lean#L56 +[TypedSystem.ofConditional]: Functional.lean#L38 +[TypedSystem.sample]: Functional.lean#L176 +[Interface.withMBO]: Game.lean#L24 +[TypedGame]: Game.lean#L35 +[TypedConverter.attachGame]: Game.lean#L38 +[PDCBehavior.liftMBO]: ../Game/MBOAttachment.lean#L455 +[TypedGame.visible]: Game.lean#L53 +[TypedGame.ofPDG]: PresentedGame.lean#L41 +[TypedGame.visible_ofPDG]: PresentedGame.lean#L51 +[TypedGame.ofSingleFunction]: PresentedGame.lean#L88 +[TypedGame.ofSingleFunction_conditionallyEquivalent]: PresentedGame.lean#L101 From 903864409759b4e750941a73d054fa50ed656bd7 Mon Sep 17 00:00:00 2001 From: Marc Ilunga Date: Tue, 13 Oct 2026 20:51:39 +0100 Subject: [PATCH 2/2] Docs: the instance table moves to the ConstructiveCryptography README THEORY.md keeps one paragraph on what instantiates the classes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9 --- THEORY.md | 138 ++----------------------- src/ConstructiveCryptography/README.md | 126 +++++++++++++++++++++- 2 files changed, 132 insertions(+), 132 deletions(-) diff --git a/THEORY.md b/THEORY.md index 9e1e6cc..5244f72 100644 --- a/THEORY.md +++ b/THEORY.md @@ -137,63 +137,16 @@ ResourceTheory ─▶ CryptographicAlgebra ─▶ CompatiblePseudoMetric ─▶ Games ─▶ DistinctionGames ``` -The table gives each class with its instance on interfaces, each field with the systems-level -object that fills it, and each axiom with the systems-level theorem that discharges it. -[ConstructiveCryptography](src/ConstructiveCryptography/README.md) states the classes, their -derived laws, and the consequences of the instances. - -| Class, instance | Field or axiom | Systems level | -|---|---|---| -| `Category` (Mathlib), [`Interface.category`][Interface.category] | objects | [interfaces][Interface] | -| | `Hom A B` | [`TypedConverter A B`][TypedConverter] | -| | `id`, `comp` | [`TypedConverter.id`][TypedConverter.id], [`TypedConverter.comp`][TypedConverter.comp]: the identity and the serial composition of PDC behaviors | -| | `id_comp`, `comp_id`, `assoc` | [`PDCBehavior.id_comp`][PDCBehavior.id_comp], [`PDCBehavior.comp_id`][PDCBehavior.comp_id], [`PDCBehavior.comp_assoc`][PDCBehavior.comp_assoc] | -| `MonoidalCategory` (Mathlib), [`Interface.monoidal`][Interface.monoidal] by `MonoidalCategory.ofTensorHom` on [`Interface.monoidalStruct`][Interface.monoidalStruct] | `tensorObj`, `tensorUnit` | [`Interface.tensor`][Interface.tensor], [`Interface.unit`][Interface.unit] | -| | `tensorHom` | [`TypedConverter.parallel`][TypedConverter.parallel], the parallel composition of PDC behaviors; `whiskerLeft` and `whiskerRight` are it with an identity | -| | `associator`, `leftUnitor`, `rightUnitor` | [`Interface.associator`][Interface.associator], [`Interface.leftUnitor`][Interface.leftUnitor], [`Interface.rightUnitor`][Interface.rightUnitor]: the [isomorphisms][Interface.isoOf] of the regrouping [renamings][TypedConverter.rename], with inverses by [`TypedConverter.rename_comp`][TypedConverter.rename_comp] and [`TypedConverter.rename_refl`][TypedConverter.rename_refl] | -| | `id_tensorHom_id` ([`Interface.id_tensor_id`][Interface.id_tensor_id]) | [`PDCBehavior.tensor_id`][PDCBehavior.tensor_id] | -| | `id_tensorHom`, `tensorHom_id` | the definition of the whiskers | -| | `tensorHom_comp_tensorHom`, interchange ([`Interface.tensor_comp`][Interface.tensor_comp]) | [`PDCBehavior.comp_tensor`][PDCBehavior.comp_tensor] | -| | `associator_naturality` ([`Interface.associator_naturality`][Interface.associator_naturality]) | [`TypedConverter.comp_associator`][TypedConverter.comp_associator] | -| | `leftUnitor_naturality`, `rightUnitor_naturality` ([left][Interface.leftUnitor_naturality], [right][Interface.rightUnitor_naturality]) | [`TypedConverter.comp_leftUnitor`][TypedConverter.comp_leftUnitor], [`TypedConverter.comp_rightUnitor`][TypedConverter.comp_rightUnitor] | -| | `pentagon`, `triangle` ([`Interface.pentagon`][Interface.pentagon], [`Interface.triangle`][Interface.triangle]) | [`TypedConverter.parallel_rename`][TypedConverter.parallel_rename] and [`TypedConverter.rename_comp`][TypedConverter.rename_comp] | -| [`ResourceTheory`][ResourceTheory]: attachment; [`Interface.resourceTheory`][Interface.resourceTheory] | carrier $`\Phi A`$ | [`TypedSystem A`][TypedSystem] | -| | `attach` | [`TypedConverter.attach`][TypedConverter.attach], the [attachment of PDC behaviors][PDCBehavior.attach] | -| | `attach_identity` | [`TypedConverter.identity_attach`][TypedConverter.identity_attach], from [`PDCBehavior.attach_id`][PDCBehavior.attach_id] | -| | `attach_serial` | [`TypedConverter.comp_smul`][TypedConverter.comp_smul], from [`PDCBehavior.attach_comp`][PDCBehavior.attach_comp] | -| [`CryptographicAlgebra`][CryptographicAlgebra]: parallel composition; [`Interface.cryptographicAlgebra`][Interface.cryptographicAlgebra] | `laxMonoidal` | [`Interface.resourcesLaxMonoidal`][Interface.resourcesLaxMonoidal] | -| | its product `μ` | [`TypedSystem.parallel`][TypedSystem.parallel], the [independent parallel composition][RandomSystem.parallel] ([`Interface.cc_parallel_eq`][Interface.cc_parallel_eq]) | -| | its unit `ε` | the [dummy typed system][TypedSystem.dummy] ([`Interface.cc_dummy_eq`][Interface.cc_dummy_eq]) | -| | `μ_natural_left`, `μ_natural_right` | [`TypedConverter.parallel_attach`][TypedConverter.parallel_attach], the locality of attachment | -| | `associativity` ([`Interface.parallel_assoc`][Interface.parallel_assoc]) | [`TypedSystem.parallel_assoc_mass`][TypedSystem.parallel_assoc_mass], through [`TypedConverter.rename_mass`][TypedConverter.rename_mass] | -| | `left_unitality`, `right_unitality` ([left][Interface.parallel_dummy_left], [right][Interface.parallel_dummy_right]) | [`TypedSystem.parallel_unit_left_mass`][TypedSystem.parallel_unit_left_mass], [`TypedSystem.parallel_unit_right_mass`][TypedSystem.parallel_unit_right_mass], through [`TypedConverter.rename_mass`][TypedConverter.rename_mass] | -| [`CompatiblePseudoMetric`][CompatiblePseudoMetric]: distance; through [`Interface.compatibleDistinguisherClass`][Interface.compatibleDistinguisherClass] | `fibreMetric` | the [advantage distance][advantageDistance] of the distinguishers below, which [is the transcript distance][Interface.cc_distance_eq] | -| | `edist_smul_le`, `edist_parallel_le` | [`CompatibleDistinguisherClass.ofClosure`][CompatibleDistinguisherClass.ofClosure] [8, Lemma 1], from the closure axioms below | -| [`CompatibleDistinguisherClass`][CompatibleDistinguisherClass]: distinguishers; [`Interface.compatibleDistinguisherClass`][Interface.compatibleDistinguisherClass] by `ofClosure` | `distinguishers A` | [`Interface.distinguishers`][Interface.distinguishers]: the maps $`R \mapsto \Pr[d(R) = 1]`$ for the [distinguisher behaviors][Domain.DistinguisherBehavior] $`d`$ compatible with $`A`$'s domain | -| | `closed_attach` ([`Interface.distinguishers_attach`][Interface.distinguishers_attach]) | [absorbing a converter][DistinguisherBehavior.absorb] | -| | `closed_parallel_left` ([`Interface.distinguishers_parallel_left`][Interface.distinguishers_parallel_left]) | [absorbing a system run beside][Domain.Distinguisher.exists_absorbRight] | -| | `closed_parallel_right` ([`Interface.distinguishers_parallel_right`][Interface.distinguishers_parallel_right]) | the previous two, through the [swap][Interface.parallel_swap], the [isomorphism][Interface.swap] of the renaming that [exchanges the two components][TypedSystem.parallel_swap_mass] | -| | `edist_eq` | the definition of the metric in `ofClosure` | -| [`Games`][Games]: games and winners; [`Interface.games`][Interface.games] | `Game A` | [`TypedGame A`][TypedGame]: the typed systems on the interface of $`A`$ with the MBO whose MBO stays set ([`RandomSystem.MonotoneMBO`][RandomSystem.MonotoneMBO]) | -| | `attachGame` | [`TypedConverter.attachGame`][TypedConverter.attachGame], the attachment of the [MBO-forwarding lift][PDCBehavior.liftMBO] | -| | `winners A` | [`Interface.winners`][Interface.winners]: the winning probabilities of the [solver behaviors][Domain.SolverBehavior] on $`A`$'s domain | -| | `attachGame_identity` | [`PDCBehavior.liftMBO_id`][PDCBehavior.liftMBO_id], with [`PDCBehavior.attach_id`][PDCBehavior.attach_id] | -| | `attachGame_serial` | [`PDCBehavior.liftMBO_comp`][PDCBehavior.liftMBO_comp], with [`PDCBehavior.attach_comp`][PDCBehavior.attach_comp] | -| | `closed_attach` | [`Domain.SolverBehavior.absorb`][Domain.SolverBehavior.absorb] | -| [`DistinctionGames`][DistinctionGames]: games and distinguishing; [`Interface.distinctionGames`][Interface.distinctionGames] | carrier, games | `TypedSystem A`, `TypedGame A` | -| | `solvers A` | [`Interface.solvers`][Interface.solvers]: the pairs of the solver behaviors on $`A`$'s domain | -| | `visible` | [`TypedGame.visible`][TypedGame.visible], the [visible system][RandomSystem.visible] | -| | `ConditionallyEquivalent` | [`RandomSystem.ConditionallyEquivalent`][RandomSystem.ConditionallyEquivalent] | -| | `solvers_winner` | the definition of the winners | -| | `solvers_closed_attach` | [`Domain.SolverBehavior.absorb`][Domain.SolverBehavior.absorb] | -| | `visible_attachGame` | [`RandomSystem.visible_attach_liftMBO`][RandomSystem.visible_attach_liftMBO] | -| | `advantage_le_win` | [`Domain.Distinguisher.advantage_le_winProbability`][Domain.Distinguisher.advantage_le_winProbability] | - -So the metric of the instance is the transcript distance of §1, $`d(R, S) = \Delta(R, S)`$, and -a typed game conditionally equivalent to a typed system $`T`$, whose MBO stays unset with -probability at least $`1 - \varepsilon`$ on fixed queries, -[has its visible typed system within][Interface.dist_visible_le] $`\varepsilon`$ of $`T`$ -[3, Theorem 4.17]. +On interfaces each class has one instance, whose fields are systems objects. The arrows of the +category are the typed converters, composed as PDC behaviors, and its monoidal product is their +parallel composition. The carrier $`\Phi A`$ is [`TypedSystem A`][TypedSystem], attachment is +[`TypedConverter.attach`][TypedConverter.attach], and the parallel composition of typed systems +is the [independent parallel composition][RandomSystem.parallel]. The distance +[is the transcript distance][Interface.cc_distance_eq] of §1, the distinguishers are the +[distinguisher behaviors][Domain.DistinguisherBehavior], and the games are the +[typed games][TypedGame]. Each axiom is discharged by a systems-level theorem; +[ConstructiveCryptography](src/ConstructiveCryptography/README.md#the-instances-on-interfaces) +lists every field and axiom with the object or theorem behind it. --- @@ -301,22 +254,15 @@ extension are in [Examples](src/Examples/README.md). [PDCBehavior.ofPDC]: src/RandomSystems/Converter/PDCBehavior.lean#L169 [PDCBehavior.comp]: src/RandomSystems/Converter/PDCBehavior.lean#L273 [PDCBehavior.id]: src/RandomSystems/Converter/PDCBehavior.lean#L369 -[PDCBehavior.comp_assoc]: src/RandomSystems/Converter/PDCBehavior.lean#L338 -[PDCBehavior.id_comp]: src/RandomSystems/Converter/PDCBehavior.lean#L385 -[PDCBehavior.comp_id]: src/RandomSystems/Converter/PDCBehavior.lean#L375 [PDCBehavior.attach]: src/RandomSystems/Converter/ConverterAttachment.lean#L156 [PDCBehavior.attach_id]: src/RandomSystems/Converter/ConverterAttachment.lean#L233 [PDCBehavior.attach_comp]: src/RandomSystems/Converter/ConverterAttachment.lean#L246 [PDCBehavior.tensor]: src/RandomSystems/Converter/ConverterTensor.lean#L649 -[PDCBehavior.comp_tensor]: src/RandomSystems/Converter/ConverterTensor.lean#L745 -[PDCBehavior.tensor_id]: src/RandomSystems/Converter/ConverterTensor.lean#L705 [Program]: src/RandomSystems/Converter/Program.lean#L45 [RandomSystem.transcriptDistance]: src/RandomSystems/Distance/Decision.lean#L228 [Domain.Distinguisher]: src/RandomSystems/Distance/Distinguisher.lean#L122 [RandomSystem.transcriptDistance_eq_iSup]: src/RandomSystems/Distance/Distinguisher.lean#L154 [Domain.DistinguisherBehavior]: src/RandomSystems/Distance/Distinguisher.lean#L207 -[DistinguisherBehavior.absorb]: src/RandomSystems/Distance/Distinguisher.lean#L291 -[Domain.Distinguisher.exists_absorbRight]: src/RandomSystems/Distance/Distinguisher.lean#L330 [RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L305 [RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L340 [RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L480 @@ -325,11 +271,6 @@ extension are in [Examples](src/Examples/README.md). [Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L756 [Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent]: src/RandomSystems/Game/MBO.lean#L874 [PDCBehavior.liftMBO]: src/RandomSystems/Game/MBOAttachment.lean#L455 -[PDCBehavior.liftMBO_id]: src/RandomSystems/Game/MBOAttachment.lean#L495 -[PDCBehavior.liftMBO_comp]: src/RandomSystems/Game/MBOAttachment.lean#L1515 -[RandomSystem.visible_attach_liftMBO]: src/RandomSystems/Game/MBOAttachment.lean#L619 -[Domain.SolverBehavior]: src/RandomSystems/Game/MBOAttachment.lean#L2169 -[Domain.SolverBehavior.absorb]: src/RandomSystems/Game/MBOAttachment.lean#L2191 @@ -339,76 +280,17 @@ extension are in [Examples](src/Examples/README.md). [TypedConverter.comp]: src/RandomSystems/Typed/Interface.lean#L134 [TypedConverter.id]: src/RandomSystems/Typed/Interface.lean#L139 [TypedConverter.attach]: src/RandomSystems/Typed/Interface.lean#L157 -[TypedConverter.identity_attach]: src/RandomSystems/Typed/Interface.lean#L171 -[TypedConverter.comp_smul]: src/RandomSystems/Typed/Interface.lean#L177 [Interface.tensor]: src/RandomSystems/Typed/Parallel.lean#L85 [TypedSystem.parallel]: src/RandomSystems/Typed/Parallel.lean#L153 [TypedConverter.parallel]: src/RandomSystems/Typed/Parallel.lean#L210 [TypedConverter.parallel_attach]: src/RandomSystems/Typed/ParallelAttachment.lean#L23 -[Interface.unit]: src/RandomSystems/Typed/InterfaceCoherence.lean#L90 [TypedConverter.rename]: src/RandomSystems/Typed/Relabel.lean#L48 -[TypedConverter.rename_comp]: src/RandomSystems/Typed/Relabel.lean#L80 -[TypedConverter.rename_refl]: src/RandomSystems/Typed/Relabel.lean#L67 -[TypedConverter.rename_mass]: src/RandomSystems/Typed/SystemParallel.lean#L55 -[TypedConverter.comp_associator]: src/RandomSystems/Typed/ConverterCoherence.lean#L158 -[TypedConverter.comp_leftUnitor]: src/RandomSystems/Typed/ConverterCoherence.lean#L195 -[TypedConverter.comp_rightUnitor]: src/RandomSystems/Typed/ConverterCoherence.lean#L224 -[TypedConverter.parallel_rename]: src/RandomSystems/Typed/TensorRename.lean#L128 -[TypedSystem.dummy]: src/RandomSystems/Typed/SystemCoherence.lean#L97 -[TypedSystem.parallel_assoc_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L85 -[TypedSystem.parallel_unit_left_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L103 -[TypedSystem.parallel_unit_right_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L128 -[TypedSystem.parallel_swap_mass]: src/RandomSystems/Typed/SystemCoherence.lean#L153 [TypedSystem.source]: src/RandomSystems/Typed/Source.lean#L51 [TypedGame]: src/RandomSystems/Typed/Game.lean#L35 -[TypedConverter.attachGame]: src/RandomSystems/Typed/Game.lean#L38 -[TypedGame.visible]: src/RandomSystems/Typed/Game.lean#L53 -[Interface.category]: src/ConstructiveCryptography/InterfaceCategory.lean#L30 -[Interface.monoidalStruct]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L71 -[Interface.monoidal]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L162 -[Interface.isoOf]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L33 -[Interface.associator]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L52 -[Interface.leftUnitor]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L57 -[Interface.rightUnitor]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L61 -[Interface.swap]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L66 -[Interface.id_tensor_id]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L84 -[Interface.tensor_comp]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L87 -[Interface.associator_naturality]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L92 -[Interface.leftUnitor_naturality]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L97 -[Interface.rightUnitor_naturality]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L101 -[Interface.pentagon]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L105 -[Interface.triangle]: src/ConstructiveCryptography/InterfaceMonoidal.lean#L132 -[ResourceTheory]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L50 -[CryptographicAlgebra]: src/ConstructiveCryptography/CryptographicAlgebra/Basic.lean#L97 -[CompatiblePseudoMetric]: src/ConstructiveCryptography/CryptographicAlgebra/PseudoMetric.lean#L43 -[advantageDistance]: src/ConstructiveCryptography/CryptographicAlgebra/Distinguisher.lean#L36 -[CompatibleDistinguisherClass]: src/ConstructiveCryptography/CryptographicAlgebra/Distinguisher.lean#L77 -[CompatibleDistinguisherClass.ofClosure]: src/ConstructiveCryptography/CryptographicAlgebra/Distinguisher.lean#L102 -[Games]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L62 -[DistinctionGames]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L112 -[Interface.resourceTheory]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L71 -[Interface.parallel_assoc]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L77 -[Interface.parallel_dummy_left]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L89 -[Interface.parallel_dummy_right]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L98 -[Interface.parallel_swap]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L107 -[Interface.resourcesLaxMonoidal]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L116 -[Interface.cryptographicAlgebra]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L142 -[Interface.distinguishers]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L148 -[Interface.distinguishers_attach]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L152 -[Interface.distinguishers_parallel_left]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L158 -[Interface.distinguishers_parallel_right]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L173 -[Interface.compatibleDistinguisherClass]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L181 -[Interface.cc_parallel_eq]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L188 -[Interface.cc_dummy_eq]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L192 [Interface.cc_distance_eq]: src/ConstructiveCryptography/InterfaceAlgebra.lean#L196 -[Interface.winners]: src/ConstructiveCryptography/InterfaceGame.lean#L58 -[Interface.solvers]: src/ConstructiveCryptography/InterfaceGame.lean#L63 -[Interface.games]: src/ConstructiveCryptography/InterfaceGame.lean#L69 -[Interface.distinctionGames]: src/ConstructiveCryptography/InterfaceGame.lean#L125 -[Interface.dist_visible_le]: src/ConstructiveCryptography/InterfaceGame.lean#L186 diff --git a/src/ConstructiveCryptography/README.md b/src/ConstructiveCryptography/README.md index 3938c82..144cbc1 100644 --- a/src/ConstructiveCryptography/README.md +++ b/src/ConstructiveCryptography/README.md @@ -7,9 +7,8 @@ carrier; the instance files `InterfaceCategory`, `InterfaceMonoidal`, `Interface `InterfaceGame` instantiate the classes on interfaces; `Substitution` is the substitution calculus; `Notation`, the proof commands of `Tactics` and the DSL front end ([GRAMMAR](DSL/GRAMMAR.md)) are built on these. The fields of the instances are the systems-level -objects of [RandomSystems](../RandomSystems/README.md), and the table of -[THEORY.md](../../THEORY.md#3-classes-and-instances) lists each field and axiom with its systems -object and theorem. Citations refer to the numbered [references](../../THEORY.md#references) of +objects of [RandomSystems](../RandomSystems/README.md), and [the table below](#the-instances-on-interfaces) lists each field and axiom with its +systems object and theorem. Citations refer to the numbered [references](../../THEORY.md#references) of THEORY.md. ## The classes @@ -116,7 +115,54 @@ and every axiom is discharged by a systems-level theorem. The instances are [`Interface.cryptographicAlgebra`][Interface.cryptographicAlgebra], [`Interface.compatibleDistinguisherClass`][Interface.compatibleDistinguisherClass], [`Interface.games`][Interface.games] and [`Interface.distinctionGames`][Interface.distinctionGames]; -the table of [THEORY.md](../../THEORY.md#3-classes-and-instances) gives each field and axiom. +the table gives each field and axiom. + +| Class, instance | Field or axiom | Systems level | +|---|---|---| +| `Category` (Mathlib), [`Interface.category`][Interface.category] | objects | [interfaces][Interface] | +| | `Hom A B` | [`TypedConverter A B`][TypedConverter] | +| | `id`, `comp` | [`TypedConverter.id`][TypedConverter.id], [`TypedConverter.comp`][TypedConverter.comp]: the identity and the serial composition of PDC behaviors | +| | `id_comp`, `comp_id`, `assoc` | [`PDCBehavior.id_comp`][PDCBehavior.id_comp], [`PDCBehavior.comp_id`][PDCBehavior.comp_id], [`PDCBehavior.comp_assoc`][PDCBehavior.comp_assoc] | +| `MonoidalCategory` (Mathlib), [`Interface.monoidal`][Interface.monoidal] by `MonoidalCategory.ofTensorHom` on [`Interface.monoidalStruct`][Interface.monoidalStruct] | `tensorObj`, `tensorUnit` | [`Interface.tensor`][Interface.tensor], [`Interface.unit`][Interface.unit] | +| | `tensorHom` | [`TypedConverter.parallel`][TypedConverter.parallel], the parallel composition of PDC behaviors; `whiskerLeft` and `whiskerRight` are it with an identity | +| | `associator`, `leftUnitor`, `rightUnitor` | [`Interface.associator`][Interface.associator], [`Interface.leftUnitor`][Interface.leftUnitor], [`Interface.rightUnitor`][Interface.rightUnitor]: the [isomorphisms][Interface.isoOf] of the regrouping [renamings][TypedConverter.rename], with inverses by [`TypedConverter.rename_comp`][TypedConverter.rename_comp] and [`TypedConverter.rename_refl`][TypedConverter.rename_refl] | +| | `id_tensorHom_id` ([`Interface.id_tensor_id`][Interface.id_tensor_id]) | [`PDCBehavior.tensor_id`][PDCBehavior.tensor_id] | +| | `id_tensorHom`, `tensorHom_id` | the definition of the whiskers | +| | `tensorHom_comp_tensorHom`, interchange ([`Interface.tensor_comp`][Interface.tensor_comp]) | [`PDCBehavior.comp_tensor`][PDCBehavior.comp_tensor] | +| | `associator_naturality` ([`Interface.associator_naturality`][Interface.associator_naturality]) | [`TypedConverter.comp_associator`][TypedConverter.comp_associator] | +| | `leftUnitor_naturality`, `rightUnitor_naturality` ([left][Interface.leftUnitor_naturality], [right][Interface.rightUnitor_naturality]) | [`TypedConverter.comp_leftUnitor`][TypedConverter.comp_leftUnitor], [`TypedConverter.comp_rightUnitor`][TypedConverter.comp_rightUnitor] | +| | `pentagon`, `triangle` ([`Interface.pentagon`][Interface.pentagon], [`Interface.triangle`][Interface.triangle]) | [`TypedConverter.parallel_rename`][TypedConverter.parallel_rename] and [`TypedConverter.rename_comp`][TypedConverter.rename_comp] | +| [`ResourceTheory`][ResourceTheory]: attachment; [`Interface.resourceTheory`][Interface.resourceTheory] | carrier $`\Phi A`$ | [`TypedSystem A`][TypedSystem] | +| | `attach` | [`TypedConverter.attach`][TypedConverter.attach], the [attachment of PDC behaviors][PDCBehavior.attach] | +| | `attach_identity` | [`TypedConverter.identity_attach`][TypedConverter.identity_attach], from [`PDCBehavior.attach_id`][PDCBehavior.attach_id] | +| | `attach_serial` | [`TypedConverter.comp_smul`][TypedConverter.comp_smul], from [`PDCBehavior.attach_comp`][PDCBehavior.attach_comp] | +| [`CryptographicAlgebra`][CryptographicAlgebra]: parallel composition; [`Interface.cryptographicAlgebra`][Interface.cryptographicAlgebra] | `laxMonoidal` | [`Interface.resourcesLaxMonoidal`][Interface.resourcesLaxMonoidal] | +| | its product `μ` | [`TypedSystem.parallel`][TypedSystem.parallel], the [independent parallel composition][RandomSystem.parallel] ([`Interface.cc_parallel_eq`][Interface.cc_parallel_eq]) | +| | its unit `ε` | the [dummy typed system][TypedSystem.dummy] ([`Interface.cc_dummy_eq`][Interface.cc_dummy_eq]) | +| | `μ_natural_left`, `μ_natural_right` | [`TypedConverter.parallel_attach`][TypedConverter.parallel_attach], the locality of attachment | +| | `associativity` ([`Interface.parallel_assoc`][Interface.parallel_assoc]) | [`TypedSystem.parallel_assoc_mass`][TypedSystem.parallel_assoc_mass], through [`TypedConverter.rename_mass`][TypedConverter.rename_mass] | +| | `left_unitality`, `right_unitality` ([left][Interface.parallel_dummy_left], [right][Interface.parallel_dummy_right]) | [`TypedSystem.parallel_unit_left_mass`][TypedSystem.parallel_unit_left_mass], [`TypedSystem.parallel_unit_right_mass`][TypedSystem.parallel_unit_right_mass], through [`TypedConverter.rename_mass`][TypedConverter.rename_mass] | +| [`CompatiblePseudoMetric`][CompatiblePseudoMetric]: distance; through [`Interface.compatibleDistinguisherClass`][Interface.compatibleDistinguisherClass] | `fibreMetric` | the [advantage distance][advantageDistance] of the distinguishers below, which [is the transcript distance][Interface.cc_distance_eq] | +| | `edist_smul_le`, `edist_parallel_le` | [`CompatibleDistinguisherClass.ofClosure`][CompatibleDistinguisherClass.ofClosure] [8, Lemma 1], from the closure axioms below | +| [`CompatibleDistinguisherClass`][CompatibleDistinguisherClass]: distinguishers; [`Interface.compatibleDistinguisherClass`][Interface.compatibleDistinguisherClass] by `ofClosure` | `distinguishers A` | [`Interface.distinguishers`][Interface.distinguishers]: the maps $`R \mapsto \Pr[d(R) = 1]`$ for the [distinguisher behaviors][Domain.DistinguisherBehavior] $`d`$ compatible with $`A`$'s domain | +| | `closed_attach` ([`Interface.distinguishers_attach`][Interface.distinguishers_attach]) | [absorbing a converter][DistinguisherBehavior.absorb] | +| | `closed_parallel_left` ([`Interface.distinguishers_parallel_left`][Interface.distinguishers_parallel_left]) | [absorbing a system run beside][Domain.Distinguisher.exists_absorbRight] | +| | `closed_parallel_right` ([`Interface.distinguishers_parallel_right`][Interface.distinguishers_parallel_right]) | the previous two, through the [swap][Interface.parallel_swap], the [isomorphism][Interface.swap] of the renaming that [exchanges the two components][TypedSystem.parallel_swap_mass] | +| | `edist_eq` | the definition of the metric in `ofClosure` | +| [`Games`][Games]: games and winners; [`Interface.games`][Interface.games] | `Game A` | [`TypedGame A`][TypedGame]: the typed systems on the interface of $`A`$ with the MBO whose MBO stays set ([`RandomSystem.MonotoneMBO`][RandomSystem.MonotoneMBO]) | +| | `attachGame` | [`TypedConverter.attachGame`][TypedConverter.attachGame], the attachment of the [MBO-forwarding lift][PDCBehavior.liftMBO] | +| | `winners A` | [`Interface.winners`][Interface.winners]: the winning probabilities of the [solver behaviors][Domain.SolverBehavior] on $`A`$'s domain | +| | `attachGame_identity` | [`PDCBehavior.liftMBO_id`][PDCBehavior.liftMBO_id], with [`PDCBehavior.attach_id`][PDCBehavior.attach_id] | +| | `attachGame_serial` | [`PDCBehavior.liftMBO_comp`][PDCBehavior.liftMBO_comp], with [`PDCBehavior.attach_comp`][PDCBehavior.attach_comp] | +| | `closed_attach` | [`Domain.SolverBehavior.absorb`][Domain.SolverBehavior.absorb] | +| [`DistinctionGames`][DistinctionGames]: games and distinguishing; [`Interface.distinctionGames`][Interface.distinctionGames] | carrier, games | `TypedSystem A`, `TypedGame A` | +| | `solvers A` | [`Interface.solvers`][Interface.solvers]: the pairs of the solver behaviors on $`A`$'s domain | +| | `visible` | [`TypedGame.visible`][TypedGame.visible], the [visible system][RandomSystem.visible] | +| | `ConditionallyEquivalent` | [`RandomSystem.ConditionallyEquivalent`][RandomSystem.ConditionallyEquivalent] | +| | `solvers_winner` | the definition of the winners | +| | `solvers_closed_attach` | [`Domain.SolverBehavior.absorb`][Domain.SolverBehavior.absorb] | +| | `visible_attachGame` | [`RandomSystem.visible_attach_liftMBO`][RandomSystem.visible_attach_liftMBO] | +| | `advantage_le_win` | [`Domain.Distinguisher.advantage_le_winProbability`][Domain.Distinguisher.advantage_le_winProbability] | Interfaces and typed converters form a category under serial composition, and a monoidal category under parallel composition. In the notation of the category, the attachment laws read @@ -414,3 +460,75 @@ compose [9, Definition 2.4.3 and Theorem 2.4.4]: a witness [substitutionRelaxation_idem]: Substitution/Relaxation.lean#L202 [Implication.exists_serial_simulators]: Substitution/Construction.lean#L44 [Constructs.derivable_serial_simulators]: Substitution/Construction.lean#L107 +[Domain.Distinguisher.advantage_le_winProbability]: ../RandomSystems/Game/MBO.lean#L756 +[Domain.Distinguisher.exists_absorbRight]: ../RandomSystems/Distance/Distinguisher.lean#L330 +[Domain.SolverBehavior.absorb]: ../RandomSystems/Game/MBOAttachment.lean#L2191 +[Interface]: ../RandomSystems/Typed/Interface.lean#L40 +[Interface.associator]: InterfaceMonoidal.lean#L52 +[Interface.associator_naturality]: InterfaceMonoidal.lean#L92 +[Interface.distinguishers]: InterfaceAlgebra.lean#L148 +[Interface.distinguishers_attach]: InterfaceAlgebra.lean#L152 +[Interface.distinguishers_parallel_left]: InterfaceAlgebra.lean#L158 +[Interface.distinguishers_parallel_right]: InterfaceAlgebra.lean#L173 +[Interface.id_tensor_id]: InterfaceMonoidal.lean#L84 +[Interface.isoOf]: InterfaceMonoidal.lean#L33 +[Interface.leftUnitor]: InterfaceMonoidal.lean#L57 +[Interface.leftUnitor_naturality]: InterfaceMonoidal.lean#L97 +[Interface.monoidalStruct]: InterfaceMonoidal.lean#L71 +[Interface.parallel_assoc]: InterfaceAlgebra.lean#L77 +[Interface.parallel_dummy_left]: InterfaceAlgebra.lean#L89 +[Interface.parallel_dummy_right]: InterfaceAlgebra.lean#L98 +[Interface.parallel_swap]: InterfaceAlgebra.lean#L107 +[Interface.pentagon]: InterfaceMonoidal.lean#L105 +[Interface.resourcesLaxMonoidal]: InterfaceAlgebra.lean#L116 +[Interface.rightUnitor]: InterfaceMonoidal.lean#L61 +[Interface.rightUnitor_naturality]: InterfaceMonoidal.lean#L101 +[Interface.solvers]: InterfaceGame.lean#L63 +[Interface.swap]: InterfaceMonoidal.lean#L66 +[Interface.tensor]: ../RandomSystems/Typed/Parallel.lean#L85 +[Interface.tensor_comp]: InterfaceMonoidal.lean#L87 +[Interface.triangle]: InterfaceMonoidal.lean#L132 +[Interface.unit]: ../RandomSystems/Typed/InterfaceCoherence.lean#L90 +[Interface.winners]: InterfaceGame.lean#L58 +[PDCBehavior.attach]: ../RandomSystems/Converter/ConverterAttachment.lean#L156 +[PDCBehavior.attach_comp]: ../RandomSystems/Converter/ConverterAttachment.lean#L246 +[PDCBehavior.attach_id]: ../RandomSystems/Converter/ConverterAttachment.lean#L233 +[PDCBehavior.comp_assoc]: ../RandomSystems/Converter/PDCBehavior.lean#L338 +[PDCBehavior.comp_id]: ../RandomSystems/Converter/PDCBehavior.lean#L375 +[PDCBehavior.comp_tensor]: ../RandomSystems/Converter/ConverterTensor.lean#L745 +[PDCBehavior.id_comp]: ../RandomSystems/Converter/PDCBehavior.lean#L385 +[PDCBehavior.liftMBO]: ../RandomSystems/Game/MBOAttachment.lean#L455 +[PDCBehavior.liftMBO_comp]: ../RandomSystems/Game/MBOAttachment.lean#L1515 +[PDCBehavior.liftMBO_id]: ../RandomSystems/Game/MBOAttachment.lean#L495 +[PDCBehavior.tensor_id]: ../RandomSystems/Converter/ConverterTensor.lean#L705 +[RandomSystem.ConditionallyEquivalent]: ../RandomSystems/Game/MBO.lean#L523 +[RandomSystem.MonotoneMBO]: ../RandomSystems/Game/MBO.lean#L305 +[RandomSystem.parallel]: ../RandomSystems/Cumulative/CumulativeOperations.lean#L130 +[RandomSystem.visible]: ../RandomSystems/Game/MBO.lean#L340 +[RandomSystem.visible_attach_liftMBO]: ../RandomSystems/Game/MBOAttachment.lean#L619 +[TypedConverter]: ../RandomSystems/Typed/Interface.lean#L127 +[TypedConverter.attach]: ../RandomSystems/Typed/Interface.lean#L157 +[TypedConverter.attachGame]: ../RandomSystems/Typed/Game.lean#L38 +[TypedConverter.comp]: ../RandomSystems/Typed/Interface.lean#L134 +[TypedConverter.comp_associator]: ../RandomSystems/Typed/ConverterCoherence.lean#L158 +[TypedConverter.comp_leftUnitor]: ../RandomSystems/Typed/ConverterCoherence.lean#L195 +[TypedConverter.comp_rightUnitor]: ../RandomSystems/Typed/ConverterCoherence.lean#L224 +[TypedConverter.comp_smul]: ../RandomSystems/Typed/Interface.lean#L177 +[TypedConverter.id]: ../RandomSystems/Typed/Interface.lean#L139 +[TypedConverter.identity_attach]: ../RandomSystems/Typed/Interface.lean#L171 +[TypedConverter.parallel]: ../RandomSystems/Typed/Parallel.lean#L210 +[TypedConverter.parallel_attach]: ../RandomSystems/Typed/ParallelAttachment.lean#L23 +[TypedConverter.parallel_rename]: ../RandomSystems/Typed/TensorRename.lean#L128 +[TypedConverter.rename]: ../RandomSystems/Typed/Relabel.lean#L48 +[TypedConverter.rename_comp]: ../RandomSystems/Typed/Relabel.lean#L80 +[TypedConverter.rename_mass]: ../RandomSystems/Typed/SystemParallel.lean#L55 +[TypedConverter.rename_refl]: ../RandomSystems/Typed/Relabel.lean#L67 +[TypedGame]: ../RandomSystems/Typed/Game.lean#L35 +[TypedGame.visible]: ../RandomSystems/Typed/Game.lean#L53 +[TypedSystem]: ../RandomSystems/Typed/Interface.lean#L92 +[TypedSystem.dummy]: ../RandomSystems/Typed/SystemCoherence.lean#L97 +[TypedSystem.parallel]: ../RandomSystems/Typed/Parallel.lean#L153 +[TypedSystem.parallel_assoc_mass]: ../RandomSystems/Typed/SystemCoherence.lean#L85 +[TypedSystem.parallel_swap_mass]: ../RandomSystems/Typed/SystemCoherence.lean#L153 +[TypedSystem.parallel_unit_left_mass]: ../RandomSystems/Typed/SystemCoherence.lean#L103 +[TypedSystem.parallel_unit_right_mass]: ../RandomSystems/Typed/SystemCoherence.lean#L128