README.md

Typed systems

This folder holds the random systems and converters of RandomSystems, 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). Every object here is a systems-level object; the instances of the classes in ConstructiveCryptography use them as their fields. Citations refer to the numbered references of THEORY.md.

Interfaces, typed systems and typed converters

An 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 $D = \lbrace h \ne \varepsilon \mid \lvert h \rvert \le q \rbrace$ and the per-port budget $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 $i$.

A typed system on $A$ is a random system on $(\Sigma_i X_i, \Sigma_i Y_i)$ over $D$, replying at the queried label. A typed converter 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. Typed converters compose by the serial composition of PDC behaviors, with the identity PDC behavior. Attachment $\alpha R$ is the attachment of the PDC behavior: the identity leaves a typed system unchanged, and a serial composition attaches its inner converter first.

Parallel interfaces put the label sets side by side, and parallel typed systems and parallel typed converters are the independent parallel compositions; attachment is local, $(\alpha \otimes \beta)(R \parallel S) = \alpha R \parallel \beta S$. A label-preserving bijection of interfaces gives a renaming, which relabels the transcripts of the typed system it is attached to; renamings compose, and the renaming by the identity is the identity. Regrouping three parallel typed systems keeps the probabilities of the regrouped transcripts, the dummy system on the interface without labels beside a typed system keeps its probabilities, on the left and on the right, and exchanging the two components of a parallel composition exchanges the labels of its transcripts. The regrouping renamings are natural for typed converters: associativity and the left and right unit regroupings commute with parallel typed converters, and the parallel composition of two renamings is the renaming of their union.

Filters, contexts, sources and functional systems

The filter admitting $D$ forwards the queries of admitted histories; it is a typed converter $(A \restriction D) \to A$ from the restricted interface. Attached to a typed system, it is the restriction of the system's random system to the restricted domain, and two filters in series act as the filter of both conditions. A constant converter ignores its inside system and exposes a fixed one, and the fixed right and left contexts run a typed system beside: attaching $\mathrm{rightContext}\ A\ S$ to $R$ gives $R \parallel S$, and so does attaching $\mathrm{leftContext}\ R\ B$ to $S$.

A 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 is a transition function with a sampled initial state [4, Definition 2], and parallel automata are the automaton running both side by side. A source is memoryless, memoryless systems side by side are memoryless, and the converter of a program maps a memoryless system to the memoryless system of its reply law, also for port-preserving programs and with its own sources beside its inside interface: the composition law of converters on their random systems. Functional systems are given by reply functions, by conditional reply laws, or by sampling once and keeping the sample.

Typed games

A typed game on $A$ is a typed system on the interface of $A$ with the MBO whose MBO, once set, stays set: a game in the sense of Game. A typed converter attaches to it through its MBO-forwarding lift, and its visible typed system is its visible system. A discrete game whose visible systems present a typed system $R$ presents a typed game on the interface of $R$, with visible typed system $R$. A single-label sampled function with a hidden condition presents a typed game whose random system is conditionally equivalent to that of the typed system sampling the ideal function, under the fixed-query factorization.