5 Supporting Theories
5.1 Polynomials
This section contains facts about polynomials that are used in the rest of the library, and also definitions for computable representations of polynomials.
We note that the Schwartz-Zippel Lemma is already in Mathlib.
We also define the type of computable univariate & multilinear polynomials using arrays to represent their coefficients (or dually, their evaluations at given points).
5.2 Coding Theory
This section contains definitions and theorems about coding theory as they are used in the rest of the library.
5.3 The VCVio Library
This library provides a formal framework for reasoning about computations that make oracle queries. Many cryptographic primitives and interactive protocols use oracles to model (or simulate) external functionality such as random responses, coin flips, or more structured queries. The VCVio library "lifts" these ideas into a setting where both the abstract specification and concrete simulation of oracles may be studied, and their probabilistic behavior analyzed.
The main ingredients of the library are as follows:
An oracle specification describes a collection of available oracles, each with its own input and output types. Formally, it’s given by an indexed family where each oracle is specified by:
A domain type (what inputs it accepts)
A range type (what outputs it can produce)
The indexing allows for potentially infinite collections of oracles, and the specification itself is agnostic to how the oracles actually behave - it just describes their interfaces.
Some examples of oracle specifications (and their intended behavior) are as follows:
emptySpec: Represents an empty set of oraclessingletonSpec: Represents a single oracle available on a singleton indexcoinSpec: A coin flipping oracle that produces a random Boolean valueunifSpec: A family of oracles that for every natural number
We often require extra properties on the domains and ranges of oracles. For example, we may require that the domains and ranges come equipped with decidable equality or finiteness properties .
An oracle computation represents a program that can make oracle queries. It can:
Return a pure value without making any queries (via pure)
Make an oracle query and continue with the response (via queryBind)
Signal failure (via failure)
The formal implementation uses a free monad on the inductive type of oracle queries wrapped in an option monad transformer (i.e. OptionT(FreeMonad(OracleQuery spec))).
To actually run oracle computations, we need a way to handle (or implement) the oracle queries. An oracle implementation consists a mapping from oracle queries to values in another monad. Depending on the monad, this may allow for various interpretations of the oracle queries.
We can view oracle computations as probabilistic programs by considering what happens when oracles respond uniformly at random. This gives rise to a probability distribution over possible outputs (including the possibility of failure). The semantics maps each oracle query to a uniform distribution over its possible responses.
Once we have mapped an oracle computation to a probability distribution, we can define various associated probabilities, such as the probability of failure, or the probability of the output satisfying a given predicate (assuming it does not fail).
We can simulate complex oracles using simpler ones by providing a translation mechanism. A simulation oracle specifies how to implement queries in one specification using computations in another specification, possibly maintaining additional state information during the simulation.
Using the simulation framework, we can add logging and caching behaviors to oracle queries:
Logging records all queries made during a computation
Caching remembers query responses and reuses them for repeated queries
These are implemented as special cases of simulation oracles.
A random oracle is implemented as a caching oracle that uses lazy sampling:
On first query: generates a uniform random response and caches it
On repeated queries: returns the cached response