Public-coin interactive oracle reductions

An interactive reduction from a relation R₁ to a relation R₂ is a public-coin protocol in which a prover convinces a verifier, who holds a statement of R₁, to output a statement of R₂, and whose prover outputs a witness for it Ben-Sasson, Chiesa and Spooner. Interactive proofs and interactive oracle proofs are the reductions to acceptance.

A protocol is described by its rounds (Interactive.Spec, a list of Interactive.Rounds). In a prover round the prover sends a message, which the verifier only accesses through the message's Interactive.OracleInterface (reading the whole message is the interface OracleInterface.full); in a verifier round the verifier sends a public random challenge, drawn from a sampler.

A prover is a strategy tree (Interactive.ProverStrategy) in the monad ProbOracleComp oP; it may draw private coins and query its oracles oP. A public-coin verifier (Interactive.Verifier) consists of one challenge sampler per verifier round and a decision: a program that queries its oracles oV and the prover's messages, given the statement and the challenges, and returns the output statement, or none to reject. A reduction from a relation R₁ to a relation R₂ (Interactive.Reduction) pairs an honest prover with a verifier.

Runs live in ProbOracleComp (oP ⊕ₒ oV); a World implements the joint oracles (the plain model, a random oracle, an ideal functionality) as one stateful handler, and World.eval gives the output law.

Shapes depend only on parameters fixed before the interaction (the index: field, sizes, circuit), never on the statement or on earlier messages. Everything indexed by a shape is defined by structural recursion on its list of rounds, so concatenated protocols compute without casts.

Main definitions

• Interactive.OracleInterface, Interactive.Round, Interactive.Spec.
• Interactive.Spec.Transcript, Interactive.Spec.PerChallenge, Interactive.Spec.MsgQuery.
• Interactive.ProverStrategy, Interactive.Prover, Interactive.Verifier, Interactive.Reduction.
• Interactive.runStrategy, Interactive.Verifier.execute, Interactive.Reduction.run.
• Interactive.World, Interactive.World.eval, Interactive.World.plain.

References

• E. Ben-Sasson, A. Chiesa, N. Spooner, Interactive Oracle Proofs

Messages and rounds

structure Cslib.Interactive.OracleInterface (M : Type) : Type 1

How the verifier accesses a prover message of type M: the queries it may ask and the responses the message gives.

• Query : Type

  The queries the verifier may ask about a message.

• Response : self.Query → Type

  The type of the response to each query.

• answer : M → (q : self.Query) → self.Response q

  The message's response to each query.

def Cslib.Interactive.OracleInterface.full (M : Type) : OracleInterface M

Reading the whole message with a single query.

def Cslib.Interactive.OracleInterface.coord (ι A : Type) : OracleInterface (ι → A)

Reading single coordinates of a vector message ι → A (as for a codeword or a PCP).

inductive Cslib.Interactive.Round : Type 1

A round of a public-coin protocol.

• prover (M : Type) (I : OracleInterface M) : Round

  The prover sends a message of type M, which the verifier accesses through I.

• verifier (C : Type) : Round

  The verifier sends a public random challenge of type C.

@[reducible, inline]

abbrev Cslib.Interactive.Round.Message : Round → Type

The type of the message sent in a round.

@[reducible, inline]

abbrev Cslib.Interactive.Spec : Type 1

A protocol specification: its rounds, in order.

@[reducible]

def Cslib.Interactive.Spec.Transcript : Spec → Type

A complete transcript: the message of every round.

@[reducible]

def Cslib.Interactive.Spec.PerChallenge (F : Type → Type) : Spec → Type

One value of F C for every verifier round with challenges in C: the challenges themselves (F = id), their samplers (F = ProbComp) or per-round errors (F = fun _ => ℝ≥0∞).

@[reducible, inline]

abbrev Cslib.Interactive.Spec.Challenges (s : Spec) : Type

The verifier's challenges in a run.

def Cslib.Interactive.Spec.Transcript.challenges (s : Spec) : s.Transcript → s.Challenges

The challenges of a transcript.

@[reducible]

def Cslib.Interactive.Spec.MsgQuery : Spec → Type

The queries the verifier may ask about the prover's messages.

@[reducible]

def Cslib.Interactive.Spec.MsgResponse (s : Spec) : s.MsgQuery → Type

The response types of the queries about the prover's messages.

@[reducible, inline]

abbrev Cslib.Interactive.Spec.msgSpec (s : Spec) : OracleSpec s.MsgQuery

The oracle interface of the prover's messages.

def Cslib.Interactive.Spec.Transcript.answer (s : Spec) : s.Transcript → (q : s.MsgQuery) → s.MsgResponse q

The prover's messages in a transcript answer the verifier's queries.

Provers and verifiers

@[reducible]

def Cslib.Interactive.ProverStrategy (m : Type → Type) : Spec → Type → Type

A strategy of a party sending the prover's messages in the rounds s, in the monad m, ending with a result of type α. In a prover round it computes a message and its continuation; in a verifier round it awaits the challenge.

@[reducible, inline]

abbrev Cslib.Interactive.Prover {ιP : Type} (oP : OracleSpec ιP) (s : Spec) (StmtIn WitIn StmtOut WitOut : Type) : Type

A prover from statements StmtIn with witnesses WitIn to statements StmtOut with witnesses WitOut, using the oracles oP.

structure Cslib.Interactive.Verifier {ιV : Type} (oV : OracleSpec ιV) (s : Spec) (StmtIn StmtOut : Type) : Type

A public-coin verifier from statements StmtIn to statements StmtOut, using the oracles oV. Its challenges are drawn from samplers. Its decision sees the statement and the challenges, queries the prover's messages and oV, and returns the output statement or rejects (none).

• samplers : Spec.PerChallenge ProbComp s

  The distribution of each challenge.

• decide : StmtIn → s.Challenges → OracleComp (oV.sum s.msgSpec) (Option StmtOut)

  The decision, with oracle access to the prover's messages.

structure Cslib.Interactive.Reduction {ιP ιV : Type} (oP : OracleSpec ιP) (oV : OracleSpec ιV) (s : Spec) (StmtIn WitIn StmtOut WitOut : Type) : Type

An interactive reduction: an honest prover and a public-coin verifier.

• prover : Prover oP s StmtIn WitIn StmtOut WitOut

  The honest prover.

• verifier : Verifier oV s StmtIn StmtOut

  The verifier.

Execution

def Cslib.Interactive.liftProver {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {α : Type} : ProbOracleComp oP α → ProbOracleComp (oP.sum oV) α

Lift a prover computation into the joint oracles.

def Cslib.Interactive.runStrategy {ιP : Type} {oP : OracleSpec ιP} {α : Type} (s : Spec) : Spec.PerChallenge ProbComp s → ProverStrategy (ProbOracleComp oP) s α → ProbOracleComp oP (s.Transcript × α)

Run a prover strategy against public challenges drawn from samplers, returning the transcript and the strategy's result.

def Cslib.Interactive.Verifier.output {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {s : Spec} {StmtIn StmtOut : Type} (V : Verifier oV s StmtIn StmtOut) (x : StmtIn) (τ : s.Transcript) : ProbOracleComp (oP.sum oV) (Option StmtOut)

Run the verifier's decision on a transcript, answering its queries about the prover's messages from the transcript.

def Cslib.Interactive.Verifier.execute {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {s : Spec} {StmtIn StmtOut α : Type} (V : Verifier oV s StmtIn StmtOut) (x : StmtIn) (P : ProbOracleComp oP (ProverStrategy (ProbOracleComp oP) s α)) : ProbOracleComp (oP.sum oV) (s.Transcript × Option StmtOut × α)

Run the verifier against any (possibly malicious) prover strategy with result type α: the transcript, the verifier's output and the prover's result.

def Cslib.Interactive.Reduction.run {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} {s : Spec} {StmtIn WitIn StmtOut WitOut : Type} (R : Reduction oP oV s StmtIn WitIn StmtOut WitOut) (x : StmtIn) (w : WitIn) : ProbOracleComp (oP.sum oV) (s.Transcript × Option StmtOut × StmtOut × WitOut)

An honest run of a reduction on x with witness w.

structure Cslib.Interactive.World {ιP ιV : Type} (oP : OracleSpec ιP) (oV : OracleSpec ιV) : Type 1

A model of the oracles: one stateful implementation of the prover's and verifier's oracles (no oracles, a random oracle, an ideal functionality).

• State : Type

  The private state of the oracles.

• init : self.State

  The initial state.

• impl (q : ιP ⊕ ιV) : StateT self.State PMF (oP.sum oV q)

  The joint implementation.

noncomputable def Cslib.Interactive.World.eval {ιP ιV : Type} {oP : OracleSpec ιP} {oV : OracleSpec ιV} (W : World oP oV) {α : Type} (program : ProbOracleComp (oP.sum oV) α) : PMF α

The output law of a program in a world.

def Cslib.Interactive.World.plain : World OracleSpec.empty OracleSpec.empty

The plain model: no oracles.