2 Oracle Reductions

2.1 Definitions

In this section, we give the basic definitions of a public-coin interactive oracle reduction (henceforth called an oracle reduction or IOR). In particular, we will define its building blocks, and various security properties.

2.1.1 Format

An (interactive) oracle reduction is an interactive protocol between two parties, a prover \(\mathcal{P}\) and a verifier \(\mathcal{V}\). It takes place in the following setting:

We work in an ambient dependent type theory (in our case, Lean).
The protocol flow is fixed and defined by a given type signature, which describes in each round which party sends a message to the other, and the type of that message.
The prover and verifier has access to some inputs (called the context) at the beginning of the protocol. These inputs are classified as follows:
- Public inputs: available to both parties;
- Private inputs (or witness): available only to the prover;
- Oracle inputs: the underlying data is available to the prover, but it’s only exposed as an oracle to the verifier. An oracle interface for such inputs consists of a query type, a response type, and a function that takes in the underlying input, a query, and outputs a response.
- Shared oracle: the oracle is available to both parties via an interface; in most cases, it is either empty, a probabilistic sampling oracle, or a random oracle. See Section 5.3 for more information on oracle computations.
The messages sent from the prover may either: 1) be seen directly by the verifier, or 2) only available to a verifier through an oracle interface (which specifies the type for the query and response, and the oracle’s behavior given the underlying message).
All messages from \(\mathcal{V}\) are chosen uniformly at random from the finite type corresponding to that round. This property is called public-coin in the literature.

We now go into more details on these objects.

Definition 1 Type Signature of an Oracle Reduction

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.

Definition 2 Context

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.

We define some supporting definitions for a protocol specification.

Definition 3 Transcript & Related Definitions

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

Remark 4 Design Decision

We do not enforce a particular interaction flow in the definition of an interactive (oracle) reduction. This is done so that we can capture all protocols in the most generality. Also, we want to allow the prover to send multiple messages in a row, since each message may have a different oracle representation (for instance, in the Plonk protocol, the prover’s first message is a 3-tuple of polynomial commitments.)

Definition 5 Type Signature of a Prover

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.

Our modeling of oracle reductions only consider public-coin verifiers; that is, verifiers who only outputs uniformly random challenges drawn from the (finite) types, and uses no other randomness. Because of this fixed functionality, we can bake the verifier’s behavior in the interaction phase directly into the protocol execution semantics.

After the interaction phase, the verifier may then run some verification procedure to check the validity of the prover’s responses. In this procedure, the verifier gets access to the public part of the context, and oracle access to either the shared oracle, or the oracle inputs.

Definition 6 Type Signature of a Verifier

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.

An oracle reduction then consists of a type signature for the interaction, and a pair of prover and verifier for that type signature.

Definition 7 Interactive Oracle Reduction

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

PL Formalization. We write our definitions in PL notation in Figure 2.1. The set of types \(\mathsf{Type}\) is the same as Lean’s dependent type theory (omitting universe levels); in particular, we care about basic dependent types (Pi and Sigma), finite natural numbers, finite fields, lists, vectors, and polynomials.

\[ \begin{array}{rcl} \mathsf{Type} & ::=& \mathsf{Unit} \mid \mathsf{Bool} \mid \mathbb {N} \mid \mathsf{Fin}\; n \mid \mathbb {F}_q \mid \mathsf{List}\; (\alpha : \mathsf{Type}) \mid (i : \iota ) \to \alpha \; i \mid (i : \iota ) \times \alpha \; i \mid \dots \\[1em] \mathsf{Dir} & ::=& \mathsf{P2V.Pub} \mid \mathsf{P2V.Orac} \mid \mathsf{V2P} \\ \mathsf{OI}\; (\mathrm{M} : \mathsf{Type}) & ::=& \langle \mathrm{Q}, \mathrm{R}, \mathrm{M} \to \mathrm{Q} \to \mathrm{R} \rangle \\ \mathsf{PSpec}\; (n : \mathbb {N}) & ::=& \mathsf{Fin}\; n \to (d : \mathsf{Dir}) \times (M : \mathsf{Type}) \times (\mathsf{if}\; d = \mathsf{P2V.Orac} \; \mathsf{then} \; \mathsf{OI}(M) \; \mathsf{else} \; \mathsf{Unit}) \\ \mathsf{OSpec} \; (\iota : \mathsf{Type}) & ::=& (i : \iota ) \to \mathsf{dom}\; i \times \mathsf{range}\; i \\[1em] \varSigma & ::=& \emptyset \mid \varSigma \times \mathsf{Type}\\ \Omega & ::=& \emptyset \mid \Omega \times \langle \mathrm{M} : \mathsf{Type}, \mathsf{OI}(\mathrm{M}) \rangle \\ \Psi & ::=& \emptyset \mid \Psi \times \mathsf{Type}\\ \end{array} \]

\[ \begin{array}{rcl} \Gamma & ::=& (\Psi ; \Omega ; \varSigma ; \rho ; \mathcal{O})\\ \mathsf{OComp}^{\mathcal{O}}\; (\alpha : \mathsf{Type}) & ::=& \mid \; \mathsf{pure}\; (a : \alpha ) \\ & & \mid \; \mathsf{queryBind}\; (i : \iota )\; (q : \mathsf{dom}\; i)\; (k : \mathsf{range}\; i \to \mathsf{OComp}^{\mathcal{O}}\; \alpha ) \\ & & \mid \; \mathsf{fail} \\[1em] \tau _{\mathsf{P}}(\Gamma ) & ::=& (i : \mathsf{Fin}\; n) \to (h : (\rho \; i).\mathsf{fst} = \mathsf{P2V}) \to \\ & & \varSigma \to \Omega \to \Psi \to \rho _{[:i]} \to \mathsf{OComp}^{\mathcal{O}}\; \left( (\rho \; i).\mathsf{snd}\right) \\[1em]\tau _{\mathsf{V}}(\Gamma ) & ::=& \varSigma \to (\rho .\mathsf{Chals}) \to \mathsf{OComp}^{\mathcal{O} :: \mathsf{OI}(\Omega ) :: \mathsf{OI}(\rho .\mathsf{Msg.Orac})}\; \mathsf{Unit} \\[1em] \tau _{\mathsf{E}}(\Gamma ) & ::=& \varSigma \to \Omega \to \rho .\mathsf{Transcript} \to \mathcal{O}.\mathsf{QueryLog} \to \Psi \end{array} \]

Figure 2.1 Type definitions for interactive oracle reductions

Using programming language notation, we can express an interactive oracle reduction as a typing judgment:

\[ \Gamma := (\Psi ; \Theta ; \varSigma ; \rho ; \mathcal{O}) \vdash \mathcal{P} : \tau _{\mathsf{P}}(\Gamma ), \; \mathcal{V} : \tau _{\mathsf{V}}(\Gamma ) \]

where:

\(\Psi \) represents the witness (private) inputs
\(\Theta \) represents the oracle inputs
\(\varSigma \) represents the public inputs (i.e. statements)
\(\mathcal{O} : \mathsf{OSpec}\; \iota \) represents the shared oracle
\(\rho : \mathsf{PSpec}\; n\) represents the protocol type signature
\(\mathcal{P}\) and \(\mathcal{V}\) are the prover and verifier, respectively, being of the given types \(\tau _{\mathsf{P}}(\Gamma )\) and \(\tau _{\mathsf{V}}(\Gamma )\).

To exhibit valid elements for the prover and verifier types, we will use existing functions in the ambient programming language (e.g. Lean).

We now define what it means to execute an oracle reduction. This is essentially achieved by first executing the prover, interspersed with oracle queries to get the verifier’s challenges (these will be given uniform random probability semantics later on), and then executing the verifier’s checks. Any message exchanged in the protocol will be added to the context. We may also log information about the execution, such as the log of oracle queries for the shared oracles, for analysis purposes (i.e. feeding information into the extractor).

Definition 8 Execution of an Oracle Reduction

Remark 9 More efficient representation of oracle reductions

The presentation of oracle reductions as protocols on an append-only context is useful for reasoning, but it does not lead to the most efficient implementation for the prover and verifier. In particular, the prover cannot keep intermediate state, and thus needs to recompute everything from scratch for each new message.

To fix this mismatch, we will also define a stateful variant of the prover, and define a notion of observational equivalence between the stateless and stateful reductions.

2.1.2 Security properties

We can now define properties of interactive reductions. The two main properties we consider in this project are completeness and various notions of soundness. We will cover zero-knowledge at a later stage.

First, for completeness, this is essentially probabilistic Hoare-style conditions on the execution of the oracle reduction (with the honest prover and verifier). In other words, given a predicate on the initial context, and a predicate on the final context, we require that if the initial predicate holds, then the final predicate holds with high probability (except for some completeness error).

Definition 10 Completeness

Almost all oracle reductions we consider actually satisfy perfect completeness, which simplifies the proof obligation. In particular, this means we only need to show that no matter what challenges are chosen, the verifier will always accept given messages from the honest prover.

For soundness, we need to consider different notions. These notions differ in two main aspects:

Whether we consider the plain soundness, or knowledge soundness. The latter relies on the notion of an extractor.
Whether we consider plain, state-restoration, round-by-round, or rewinding notion of soundness.

We note that state-restoration knowledge soundness is necessary for the security of the SNARK protocol obtained from the oracle reduction after composing with a commitment scheme and applying the Fiat-Shamir transform. It in turn is implied by either round-by-round knowledge soundness, or special soundness (via rewinding). At the moment, we only care about non-rewinding soundness, so mostly we will care about round-by-round knowledge soundness.

Definition 11 Soundness

A (straightline) extractor for knowledge soundness is a deterministic algorithm that takes in the output public context after executing the oracle reduction, the side information (i.e. log of oracle queries from the malicious prover) observed during execution, and outputs the witness for the input context.

Note that since we assume the context is append-only, and we append only the public (or oracle) messages obtained during protocol execution, it follows that the witness stays the same throughout the execution.

Definition 12 Knowledge Soundness

To define round-by-round (knowledge) soundness, we need to define the notion of a state function. This is a (possibly inefficient) function \(\mathsf{StateF}\) that, for every challenge sent by the verifier, takes in the transcript of the protocol so far and outputs whether the state is doomed or not. Roughly speaking, the requirement of round-by-round soundness is that, for any (possibly malicious) prover \(P\), if the state function outputs that the state is doomed on some partial transcript of the protocol, then the verifier will reject with high probability.

Definition 13 State Function

Definition 14 Round-by-Round Soundness

Definition 15 Round-by-Round Knowledge Soundness

By default, the properties we consider are perfect completeness and (straightline) round-by-round knowledge soundness. We can encapsulate these properties into the following typing judgement:

\[ \Gamma := (\Psi ; \Theta ; \varSigma ; \rho ; \mathcal{O}) \vdash \{ \mathcal{R}_1\} \quad \langle \mathcal{P}, \mathcal{V}, \mathcal{E}\rangle \quad \{ \! \! \{ \mathcal{R}_2; \mathsf{St}; \epsilon \} \! \! \} \]

2.2 A Program Logic for Oracle Reductions

In this section, we describe a program logic for reasoning about oracle reductions. In other words, we define a number of rules (or theorems) that govern how oracle reductions can be composed to form larger reductions, and how the resulting reduction inherits the security properties of the components.

The first group of rules changes relations and shared oracles.

2.2.1 Changing Relations and Oracles

Here we express the consequence rule. Namely, if we have an oracle reduction for \(\mathcal{R}_1 \implies \mathcal{R}_2\), along with \(\mathcal{R}_1' \implies \mathcal{R}_1\) and \(\mathcal{R}_2 \implies \mathcal{R}_2'\), then we obtain an oracle reduction for \(\mathcal{R}_1' \implies \mathcal{R}_2'\).

\[ \frac{\begin{array}{c} \Psi ; \Theta ; \Sigma \vdash \{ \mathcal{R}_1\} \; \langle \mathcal{P},\, \mathcal{V},\, \mathcal{E}\rangle ^{\mathcal{O}} : \tau \; \{ \! \! \{ \mathcal{R}_2; \, \mathsf{St};\, \epsilon \} \! \! \} \\[1.5ex] \mathcal{R}_1’ \implies \mathcal{R}_1 \\[1.5ex] \mathcal{R}_2 \implies \mathcal{R}_2’ \end{array}}{\Psi ; \Theta ; \Sigma \vdash \{ \mathcal{R}_1'\} \; \langle \mathcal{P},\, \mathcal{V},\, \mathcal{E}\rangle ^{\mathcal{O}} : \tau \; \{ \! \! \{ \mathcal{R}_2'; \, \mathsf{St};\, \epsilon \} \! \! \} } \quad \text{(Conseq)} \]

\[ \frac{\Psi ; \Theta ; \Sigma \vdash \{ \mathcal{R}_1\} \; \langle \mathcal{P}, \mathcal{V}, \mathcal{E}\rangle ^{\mathcal{O}} : \tau \; \{ \! \! \{ \mathcal{R}_2; \mathsf{St}; \epsilon \} \! \! \} }{\Psi ; \Theta ; \Sigma \vdash \{ \mathcal{R} \times \mathcal{R}_1\} \; \langle \mathcal{P}, \mathcal{V}, \mathcal{E}\rangle ^{\mathcal{O}} : \tau \; \{ \! \! \{ \mathcal{R} \times \mathcal{R}_2; \mathsf{St}; \epsilon \} \! \! \} } \quad \text{(Frame)} \]

\[ \frac{\begin{array}{c} \Psi ; \Theta ; \Sigma \vdash \{ \mathcal{R}_1\} \; \langle \mathcal{P}, \mathcal{V}, \mathcal{E}\rangle ^{\mathcal{O}_1} : \tau \; \{ \! \! \{ \mathcal{R}_2; \mathsf{St}; \epsilon \} \! \! \} \\[1.5ex] \mathcal{O}_1 \subset \mathcal{O}_2 \end{array}}{\Psi ; \Theta ; \Sigma \vdash \{ \mathcal{R}_1\} \; \langle \mathcal{P}, \mathcal{V}, \mathcal{E}\rangle ^{\mathcal{O}_2} : \tau \; \{ \! \! \{ \mathcal{R}_2; \mathsf{St}; \epsilon \} \! \! \} } \quad \text{(Oracle-Lift)} \]

TODO: figure out how the state function needs to change for these rules (they are basically the same, but not exactly)

2.2.2 Sequential Composition

The reason why we consider interactive (oracle) reductions at the core of our formalism is that we can compose these reductions to form larger reductions. Equivalently, we can take a complex interactive (oracle) proof (which differs only in that it reduces a relation to the trivial relation that always outputs true) and break it down into a series of smaller reductions. The advantage of this approach is that we can prove security properties (completeness and soundness) for each of the smaller reductions, and these properties will automatically transfer to the larger reductions.

This section is devoted to the composition of interactive (oracle) reductions, and proofs that the resulting reductions inherit the security properties of the two (or more) constituent reductions.

Sequential composition can be expressed as the folowing rule:

\[ \frac{\begin{array}{c} \Psi ; \Theta ; \varSigma \vdash \{ \mathcal{R}_1\} \; \langle \mathcal{P}_1, \mathcal{V}_1, \mathcal{E}_1\rangle ^{\mathcal{O}} : \tau _1 \; \{ \! \! \{ \mathcal{R}_2; \mathsf{St}_1; \epsilon _1\} \! \! \} \\[1.5ex] \Psi ; (\Theta :: \tau _1) ; \varSigma \vdash \{ \mathcal{R}_2\} \; \langle \mathcal{P}_2, \mathcal{V}_2, \mathcal{E}_2\rangle ^{\mathcal{O}} : \tau _2 \; \{ \! \! \{ \mathcal{R}_3; \mathsf{St}_2; \epsilon _2\} \! \! \} \end{array}}{\Psi ; (\Theta :: \tau _1 :: \tau _2) \ ; \varSigma \vdash \{ \mathcal{R}_1\} \; \langle \mathcal{P}_1 \circ \mathcal{P}_2, \mathcal{V}_1 \circ \mathcal{V}_2, \mathcal{E}_1 \circ _{\mathcal{V}_2} \mathcal{E}_2\rangle ^{\mathcal{O}} : \tau _1 \oplus \tau _2 \; \{ \! \! \{ \mathcal{R}_3; \mathsf{St}_1 \oplus \mathsf{St}_2; \epsilon _1 \oplus \epsilon _2\} \! \! \} } \quad \text{(Seq-Comp)} \]

2.2.3 Virtualization

Another tool we will repeatedly use is the ability to change the context of an oracle reduction. This is often needed when we want to adapt an oracle reduction in a simple context into one for a more complex context.

See the section on sum-check 3.2 for an example.

Definition 16 Mapping into Virtual 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.

Definition 17 Virtual Oracle Reduction

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.

We will show security properties for this virtualization process. One can see that completeness and soundness are inherited from the completeness and soundness of the virtual oracle reduction. However, (round-by-round) knowledge soundness is more tricky; this is because we must extract back to the witness of the original context from the virtual context.

\[ \frac{\begin{array}{c} \Psi ’; \Theta ’; \Sigma ’ \vdash \{ \mathcal{R}_1\} \; \langle \mathcal{P}, \mathcal{V}, \mathcal{E}\rangle ^{\mathcal{O}} : \tau \; \{ \! \! \{ \mathcal{R}_2; \mathsf{St}; \epsilon \} \! \! \} \\[1.5ex] f : (\Psi , \Theta , \Sigma ) \to (\Psi ’, \Theta ’, \Sigma ’) \\[1.5ex] g : \Psi ’ \to \Psi \\[1.5ex] f.\mathsf{fst} \circ g = \mathsf{id} \end{array}}{\Psi ; \Theta ; \Sigma \vdash \{ \mathcal{R}_1 \circ f\} \; \langle \mathcal{P} \circ f, \mathcal{V} \circ f, \mathcal{E} \circ (f, g)\rangle ^{\mathcal{O}} : \tau \; \{ \! \! \{ \mathcal{R}_2 \circ f; \mathsf{St} \circ f; \epsilon \} \! \! \} } \quad \text{(Virtual-Ctx)} \]

2.2.4 Substitution

Finally, we need a transformation / inference rule that allows us to change the message type in a given round of an oracle reduction. In other words, we substitute a value in the round with another value, followed by a reduction establishing the relationship between the new and old values.

Examples include:

Substituting an oracle input by a public input:
- Often by just revealing the underlying data. This has no change on the prover, and for the verifier, this means that any query to the oracle input can be locally computed.
- A variant of this is when the oracle input consists of a data along with a proof that the data satisfies some predicate. In this case, the verifier needs to additionally check that the predicate holds for the substituted data.
- Another common substitution is to replace a vector with its Merkle commitment, or a polynomial with its polynomial commitment.
Substituting an oracle input by another oracle input, followed by a reduction for each oracle query the verifier makes to the old oracle:
- This is also a variant of the previous case, where we do not fully substitute with a public input, but do a “half-substitution” by substituting with another oracle input. This happens e.g. when using a polynomial commitment scheme that is itself based on a vector commitment scheme. One can cast protocols like Ligero / Brakedown / FRI / STIR in this two-step process.