Definitions and Instances for OracleInterface

We define OracleInterface, which is a type class that augments a type with an oracle interface for that type. The interface specifies the type of queries, the type of responses, and the oracle's behavior for a given underlying element of the type.

OracleInterface is used to restrict the verifier's access to the input oracle statements and the prover's messages in an interactive oracle reduction (see Basic.lean).

We define OracleInterface instances for common types:

• Univariate and multivariate polynomials. These instances turn polynomials into oracles for which one can query at a point, and the response is the evaluation of the polynomial on that point.

• Vectors. This instance turns vectors into oracles for which one can query specific positions.

class OracleInterface (Message : Type u) : Type (max (u + 1) (v + 1))

OracleInterface is a type class that provides an oracle interface for a type Message. It consists of:

• a query type Query,
• a response type Response,
• a function answer that given a message m : Message and a query q : Query, returns a response r : Response.

TODO: turn (Query, Response) into a general PFunctor (i.e. Response : Query → Type) This allows for better compositionality of OracleInterface, including (indexed) sum, instead of requiring indexed family of OracleInterfaces.

However, this won't be possible until OracleSpec is changed to be an alias for PFunctor

dtumad: Eventually I think we should directly use OracleContext instead?

• Query : Type v
• toOC : OracleContext (Query Message) (ReaderM Message)

theorem OracleInterface.ext {Message : Type u} {x y : OracleInterface Message} (Query : Query Message = Query Message) (toOC : toOC ≍ toOC) : x = y

theorem OracleInterface.ext_iff {Message : Type u} {x y : OracleInterface Message} : x = y ↔ Query Message = Query Message ∧ toOC ≍ toOC

def OracleContext.ofFunction (α : Type u_1) (β : Type (max u_2 u_1)) : OracleContext α (ReaderM (α → β))

def OracleInterface.Response {Message : Type u_1} [O : OracleInterface Message] (q : Query Message) : Type u_1

def OracleInterface.spec {Message : Type u_1} [O : OracleInterface Message] : OracleSpec (Query Message)

def OracleInterface.answer {Message : Type u_1} [O : OracleInterface Message] (m : Message) (q : Query Message) : Response q

def OracleInterface.instDefault {Message : Type u} : OracleInterface Message

The default instance for OracleInterface, where the query is trivial (a Unit) and the response returns the data. We do not register this as an instance, instead explicitly calling it where necessary.

@[implicit_reducible]

instance OracleInterface.instInhabited {Message : Type u_1} : Inhabited (OracleInterface Message)

def OracleInterface.toOracleSpec {ι : Type u} (v : ι → Type v) [O : (i : ι) → OracleInterface (v i)] : OracleSpec ((i : ι) × Query (v i))

Converts an indexed type family of oracle interfaces into an oracle specification.

Notation: [v]ₒ for when the oracle interfaces can be inferred, and [v]ₒ'O for when the oracle interfaces need to be specified.

def OracleInterface.«term[_]ₒ» : Lean.ParserDescr

Converts an indexed type family of oracle interfaces into an oracle specification.

Notation: [v]ₒ for when the oracle interfaces can be inferred, and [v]ₒ'O for when the oracle interfaces need to be specified.

def OracleInterface.«term[_]ₒ'_» : Lean.ParserDescr

Converts an indexed type family of oracle interfaces into an oracle specification.

Notation: [v]ₒ for when the oracle interfaces can be inferred, and [v]ₒ'O for when the oracle interfaces need to be specified.

def OracleInterface.toOracleImpl {ι : Type u} (v : ι → Type v) [O : (i : ι) → OracleInterface (v i)] (data : (i : ι) → v i) : QueryImpl [v]ₒ Id

Given an underlying data for an indexed type family of oracle interfaces v, we can give an implementation of all queries to the interface defined by v

@[implicit_reducible]

instance OracleInterface.instElim0 (i : Fin 0) : OracleInterface i.elim0

Any function type has a canonical OracleInterface instance, whose answer is the function itself.

@[reducible, inline]

instance OracleInterface.instFunction {α : Type u_1} {β : Type (max u_1 u_2)} : OracleInterface (α → β)

@[implicit_reducible]

instance OracleInterface.instDecidableEqSigmaQueryToOracleSpecOfDecidableEqResponse {ι : Type u} [DecidableEq ι] (v : ι → Type v) [O : (i : ι) → OracleInterface (v i)] [h : (i : ι) → DecidableEq (Query (v i))] [h' : (i : ι) → (q : Query (v i)) → DecidableEq (Response q)] : [v]ₒ.DecidableEq

@[implicit_reducible]

instance OracleInterface.instFintypeSigmaQueryToOracleSpecOfFintypeResponse {ι : Type u} (v : ι → Type v) [O : (i : ι) → OracleInterface (v i)] [h : (i : ι) → (q : Query (v i)) → Fintype (Response q)] : [v]ₒ.Fintype

@[implicit_reducible]

instance OracleInterface.instInhabitedSigmaQueryToOracleSpecOfInhabitedResponse {ι : Type u} (v : ι → Type v) [O : (i : ι) → OracleInterface (v i)] [h : (i : ι) → (q : Query (v i)) → Inhabited (Response q)] : [v]ₒ.Inhabited

@[reducible, inline]

instance OracleInterface.instRecType {ι₁ : Type u} {T₁ : ι₁ → Type v} [inst₁ : (i : ι₁) → OracleInterface (T₁ i)] {ι₂ : Type u} {T₂ : ι₂ → Type v} [inst₂ : (i : ι₂) → OracleInterface (T₂ i)] (i : ι₁ ⊕ ι₂) : OracleInterface (Sum.rec T₁ T₂ i)

@[reducible, inline, instance 100]

instance OracleInterface.instTensorProd {α : Type u_1} {β : Type u_2} [Oα : OracleInterface α] [Oβ : OracleInterface β] : OracleInterface (α × β)

The tensor product oracle interface for the product of two types α and β, each with its own oracle interface, is defined as:

• The query & response types are the product of the two query & response types.
• The oracle will run both oracles and return the pair of responses.

This is a low priority instance since we do not expect to have this behavior often. See instProd for the sum behavior on the interface.

@[reducible, inline]

instance OracleInterface.instProd {α β : Type} [Oα : OracleInterface α] [Oβ : OracleInterface β] : OracleInterface (α × β)

The product oracle interface for the product of two types α and β, each with its own oracle interface, is defined as:

• The query & response types are the sum type of the two query & response types.
• The oracle will answer depending on the input query.

This is the behavior more often assumed, i.e. when we send multiple oracle messages in a round. See instTensor for the tensor product behavior on the interface.

@[reducible, inline, instance 100]

instance OracleInterface.instTensorForall {ι : Type u} (v : ι → Type (max u_1 u)) [O : (i : ι) → OracleInterface (v i)] : OracleInterface ((i : ι) → v i)

The indexed tensor product oracle interface for the dependent product of a type family v, indexed by ι, each having an oracle interface, is defined as:

• The query & response types are the dependent product of the query & response types of the type family.
• The oracle, on a given query specifying the index i of the type family, will run the oracle of v i and return the response.

This is a low priority instance since we do not expect to have this behavior often. See instProdForall for the product behavior on the interface (with dependent sums for the query and response types).

@[reducible, inline]

instance OracleInterface.instProdForall {ι : Type u} (v : ι → Type (max u_1 u)) [O : (i : ι) → OracleInterface (v i)] : OracleInterface ((i : ι) → v i)

The indexed product oracle interface for the dependent product of a type family v, indexed by ι, each having an oracle interface, is defined as:

• The query & response types are the dependent product of the query & response types of the type family.
• The oracle, on a given query specifying the index i of the type family, will run the oracle of v i and return the response.

This is the behavior usually assumed, i.e. when we send multiple oracle messages in a round. See instTensorForall for the tensor product behavior on the interface.

def OracleInterface.simOracle0 {ι : Type u_1} (T : ι → Type u_2) [O : (i : ι) → OracleInterface (T i)] (t : (i : ι) → T i) : QueryImpl [T]ₒ Id

Auto apply the ReaderM monad in the underlying QueryImpl to get an Id final monad.

def OracleInterface.simOracle {ι : Type u} (oSpec : OracleSpec ι) {ι' : Type v} {T : ι' → Type w} [(i : ι') → OracleInterface (T i)] (t : (i : ι') → T i) : QueryImpl (oSpec + [T]ₒ) (OracleComp oSpec)

Combines multiple oracle specifications into a single oracle by routing queries to the appropriate underlying oracle. Takes:

• A base oracle specification oSpec
• An indexed type family T with OracleInterface instances
• Values of that type family Returns a stateless oracle that routes queries to the appropriate underlying oracle.

def OracleInterface.simOracle2 {ι : Type u} (oSpec : OracleSpec ι) {ι₁ : Type v} {T₁ : ι₁ → Type w} [(i : ι₁) → OracleInterface (T₁ i)] {ι₂ : Type v} {T₂ : ι₂ → Type w} [(i : ι₂) → OracleInterface (T₂ i)] (t₁ : (i : ι₁) → T₁ i) (t₂ : (i : ι₂) → T₂ i) : QueryImpl (oSpec + ([T₁]ₒ + [T₂]ₒ)) (OracleComp oSpec)

Combines multiple oracle specifications into a single oracle by routing queries to the appropriate underlying oracle. Takes:

• A base oracle specification oSpec
• Two indexed type families T₁ and T₂ with OracleInterface instances
• Values of those type families Returns a stateless oracle that routes queries to the appropriate underlying oracle.

def OracleInterface.distanceLE {Message : Type u_1} (O : OracleInterface Message) [Fintype (Query Message)] [(q : Query Message) → DecidableEq (toOC.spec q)] (d : ℕ) : Prop

A message type together with a OracleInterface instance is said to have oracle distance (at most) d if for any two distinct messages, there is at most d queries that distinguish them, i.e.

#{q | OracleInterface.answer a q = OracleInterface.answer b q} ≤ d.

This property corresponds to the distance of a code, when the oracle instance is to encode the message and the query is a position of the codeword. In particular, it applies to (Mv)Polynomial.

@[reducible, inline]

instance OracleInterface.instPolynomial (R : Type u_2) [CommSemiring R] : OracleInterface (Polynomial R)

Univariate polynomials can be accessed via evaluation queries.

@[reducible, inline]

instance OracleInterface.instPolynomialDegreeLE (R : Type u_2) [CommSemiring R] (d : ℕ) : OracleInterface ↥(Polynomial.degreeLE R ↑d)

Univariate polynomials with degree at most d can be accessed via evaluation queries.

@[reducible, inline]

instance OracleInterface.instPolynomialDegreeLT (R : Type u_2) [CommSemiring R] (d : ℕ) : OracleInterface ↥(Polynomial.degreeLT R d)

Univariate polynomials with degree less than d can be accessed via evaluation queries.

@[implicit_reducible]

noncomputable instance OracleInterface.instMvPolynomial (R : Type (max u_2 u_1)) [CommSemiring R] (σ : Type u_1) : OracleInterface (MvPolynomial σ R)

Multivariate polynomials can be accessed via evaluation queries.

@[implicit_reducible]

noncomputable instance OracleInterface.instMvPolynomialDegreeLE (R : Type (max u_2 u_1)) [CommSemiring R] (d : ℕ) (σ : Type u_1) : OracleInterface ↥(MvPolynomial.restrictDegree σ R d)

Multivariate polynomials with individual degree at most d can be accessed via evaluation queries.

@[implicit_reducible]

instance OracleInterface.instFintypeQuerySubtypeMvPolynomialMemSubmoduleRestrictDegreeOfDecidableEq (R : Type (max u_1 u_2)) [CommSemiring R] (d : ℕ) (σ : Type u_1) [Fintype σ] [DecidableEq σ] [Fintype R] : Fintype (Query ↥(MvPolynomial.restrictDegree σ R d))

@[implicit_reducible]

instance OracleInterface.instListVector {n : ℕ} {α : Type u_1} : OracleInterface (List.Vector α n)

Vectors of the form List.Vector α n can be accessed via queries on their indices.

@[implicit_reducible]

instance OracleInterface.instVector {n : ℕ} {α : Type u_1} : OracleInterface (Vector α n)

Vectors of the form Vector α n can be accessed via queries on their indices.

@[simp]

theorem distanceLE_polynomial_degreeLT {R : Type u_1} [CommRing R] {d : ℕ} [Fintype R] [DecidableEq R] [IsDomain R] : (OracleInterface.instPolynomialDegreeLT R d).distanceLE (d - 1)

theorem distanceLE_polynomial_degreeLE {R : Type u_1} [CommRing R] {d : ℕ} [Fintype R] [DecidableEq R] [IsDomain R] : (OracleInterface.instPolynomialDegreeLT R d).distanceLE d

theorem distanceLE_mvPolynomial_degreeLE {R : Type u_1} [CommRing R] {d : ℕ} [Fintype R] [DecidableEq R] [IsDomain R] {σ : Type} [Fintype σ] [DecidableEq σ] : (OracleInterface.instMvPolynomialDegreeLE R d σ).distanceLE (Fintype.card σ * d * Fintype.card R ^ (Fintype.card σ - 1))

Schwartz-Zippel-type distance bound for multivariable polynomials of degree ≤ d. The bound is Fintype.card σ * d * Fintype.card R ^ (Fintype.card σ - 1) (the earlier bound Fintype.card σ * d was false; see counterexample in comment history).