Dependencies

The sum-check protocol is complete.

In an oracle reduction, its context (denoted \(\Gamma \)) consists of a list of public inputs, a list of witness inputs, a list of oracle inputs, and a shared oracle (possibly represented as a list of lazily sampled query-response pairs). These inputs have the expected visibility.

For simplicity, we imagine the context as append-only, as we add new messages from the protocol execution.

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.

An interactive oracle reduction for a given context \(\Gamma \) is a combination a prover and a verifier of the types specified above.

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.

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))).

A protocol specification \(\rho : \mathsf{PSpec}\; n\) of an oracle reduction is parametrized by a fixed number of messages sent in total. For each step of interaction, it specifies a direction for the messsage (prover to verifier, or vice versa), and a type for the message. If a message from the prover to the verifier is further marked as oracle, then we also expect an oracle interface for that message. In Lean, we handle these oracle interfaces via the \(\mathsf{ToOracle}\) type class.

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.

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.

A prover \(\mathcal{P}\) in an oracle reduction, given a context, is a stateful oracle computation that at each step of the protocol, either takes in a new message from the verifier, or sends a new message to the verifier.

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

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.

Given protocol specification \(\rho : \mathsf{PSpec}\; n\), its transcript up to round \(i\) is an element of type \(\rho _{[:i]} ::= \prod _{j {\lt} i} \rho \; j\). We define the type of all challenges sent by the verifier as \(\rho .\mathsf{Chals} ::= \prod _{i \text{ s.t. } (\rho \; i).\mathsf{fst} = \mathsf{V2P}} (\rho \; i).\mathsf{snd}\).

A verifier \(\mathcal{V}\) in an oracle reduction is an oracle computation that may perform a series of checks (i.e. ‘Bool‘-valued, or ‘Option Unit‘) on the given context.

In order to apply an oracle reduction on virtual data, we will need to provide a mapping from the current context to the virtual context. This includes:

• A mapping from the current public inputs to the virtual public inputs.

• A simulation of the oracle inputs for the virtual context using the public and oracle inputs for the current context.

• A mapping from the current private inputs to the virtual private inputs.

• A simulation of the shared oracle for the virtual context using the shared oracle for the current context.

Given a suitable mapping into a virtual context, we may define an oracle reduction via the following construction:

• The prover first applies the mappings to obtain the virtual context. The verifier does the same, but only for the non-private inputs.

• The prover and verifier then run the virtual oracle reduction on the virtual context.