Interactive (Oracle) Reductions

This file defines the basic components of a public-coin Interactive Oracle Reduction (IOR). These are interactive protocols between two parties, a prover and a verifier, with the following format:

• The protocol proceeds over a number of steps. In each step, either the prover or the verifier sends a message to the other. We assume that this sequence of interactions is fixed in advance, and is described by a protocol specification (see ProtocolSpec.lean).

  Note that we do not require interleaving prover's messages with verifier's challenges, for maximum flexibility in defining reductions.

• Both parties may have access to some shared oracle, which is modeled as an oracle specification OracleSpec. These are often probabilistic sampling or random oracles.

• At the beginning, the prover and verifier both take in an input statement StmtIn. There are a number of input oracle statements OStmtIn whose underlying content is known to the prover, but is only available via an oracle interface to the verifier. The prover also takes in a private witness WitIn.

• During the interaction, the verifier is assumed to always send uniformly random challenges to the prover. The prover will send messages, which is either available in full to the verifier, or received as oracles. Which is which is specified by the protocol specification.

• At the end of the interaction, the verifier performs a computation that outputs a new statement StmtOut, and specify a subset of the oracles it has received to be the output oracle statements.

Our formulation of IORs can be seen in the literature as F-IORs, where F denotes an arbitrary class of oracles. See the blueprint for more details about our modeling choices.

We can then specialize our definition to obtain specific instantiations in the literature:

• Interactive Reductions (IRs) are a special kind of IORs where all of the prover's messages are available in full.
• Interactive Oracle Proofs (IOPs) are a special kind of IORs where the output statement is Boolean (i.e. accept/reject), there is no oracle output statements, and the output witness is trivial.
• Further specialization of IOPs include Vector IOPs, Polynomial IOPs, and so on, are defined in downstream files. Note that vector IOPs is the original definition of IOPs [BCS16], while polynomial IOPs were later introduced in [BCG+19] and others.
• Interactive Proofs (IPs) are a combination of IRs and IOPs.
• Non-Interactive Reductions (for example, folding or accumulation schemes) are IRs with a single message from the prover.
• Non-Interactive Arguments of Knowledge (NARKs) are IPs with a single message from the prover.

We note that this file only defines the type signature of IORs. The semantics of executing an IOR can be found in Execution.lean, while the security notions are found in the Security folder.

Note the appearance of the various dependencies in the type signatures:

• oSpec : OracleSpec ι comes first, as we expect this to be the ambient (fixed) shared oracle specification for the protocol
• StmtIn comes next, as the type of the input statement to the protocol
• Then we have OStmtIn for the type of the oracle input statements (for oracle reductions), followed by WitIn, the type of the input witness
• Then we have StmtOut for the type of the output statement, followed by OStmtOut for the type of the output oracle statements, and finally WitOut for the type of the output witness
• Finally, we have pSpec : ProtocolSpec n, which is the protocol specification for the (oracle) reduction

We arrange things in this way for potential future extensions, where later types may depend on earlier types (i.e. WitIn, StmtOut, or pSpec may depend on StmtIn; though we do not expect, say, StmtOut or pSpec to depend on the witness types, as that is not available to the (oracle) verifier).

structure Indexer {ι : Type} (oSpec : OracleSpec ι) {n : ℕ} (pSpec : ProtocolSpec n) (Index Encoding : Type) : Type (max 1 u_1)

• encode : Index → OracleComp oSpec Encoding
• OracleInterface : _root_.OracleInterface Encoding

structure ProverState (n : ℕ) : Type 1

The type signature for the prover's state at each round.

For a protocol with n messages exchanged, there will be (n + 1) prover states, with the first state before the first message and the last state after the last message.

• PrvState : Fin (n + 1) → Type

theorem ProverState.ext_iff {n : ℕ} {x y : ProverState n} : x = y ↔ x.PrvState = y.PrvState

theorem ProverState.ext {n : ℕ} {x y : ProverState n} (PrvState : x.PrvState = y.PrvState) : x = y

structure ProverInput (StmtIn WitIn PrvState : Type) : Type

Initialization of prover's state via inputting the statement and witness.

• input : StmtIn × WitIn → PrvState

theorem ProverInput.ext_iff {StmtIn WitIn PrvState : Type} {x y : ProverInput StmtIn WitIn PrvState} : x = y ↔ x.input = y.input

theorem ProverInput.ext {StmtIn WitIn PrvState : Type} {x y : ProverInput StmtIn WitIn PrvState} (input : x.input = y.input) : x = y

structure ProverInit (PrvState : Type) : Type

• init : PrvState

structure ProverRound {ι : Type} (oSpec : OracleSpec ι) {n : ℕ} (pSpec : ProtocolSpec n) extends ProverState n : Type (max 1 u_1)

Represents the interaction of a prover for a given protocol specification.

In each step, the prover gets access to the current state, then depending on the direction of the step, the prover either sends a message or receives a challenge, and updates its state accordingly.

For maximum simplicity, we only define the sendMessage function as an oracle computation. All other functions are pure. We may revisit this decision in the future.

• PrvState : Fin (n + 1) → Type
• sendMessage (i : pSpec.MessageIdx) : self.PrvState (↑i).castSucc → OracleComp oSpec (pSpec.Message i × self.PrvState (↑i).succ)

  Send a message and update the prover's state

• receiveChallenge (i : pSpec.ChallengeIdx) : self.PrvState (↑i).castSucc → OracleComp oSpec (pSpec.Challenge i → self.PrvState (↑i).succ)

  Receive a challenge and update the prover's state

theorem ProverRound.ext {ι : Type} {oSpec : OracleSpec ι} {n : ℕ} {pSpec : ProtocolSpec n} {x y : ProverRound oSpec pSpec} (PrvState : x.PrvState = y.PrvState) (sendMessage : x.sendMessage ≍ y.sendMessage) (receiveChallenge : x.receiveChallenge ≍ y.receiveChallenge) : x = y

theorem ProverRound.ext_iff {ι : Type} {oSpec : OracleSpec ι} {n : ℕ} {pSpec : ProtocolSpec n} {x y : ProverRound oSpec pSpec} : x = y ↔ x.PrvState = y.PrvState ∧ x.sendMessage ≍ y.sendMessage ∧ x.receiveChallenge ≍ y.receiveChallenge

structure ProverOutput {ι : Type} (oSpec : OracleSpec ι) (Output PrvState : Type) : Type u_1

The output function of the prover, which takes in the prover's final state and returns an oracle computation that outputs some specified output type Output

We note that an honest prover may output both the output statement and witness (for easier composability), but an adversarial prover in the knowledge soundness game may only output the witness.

• output : PrvState → OracleComp oSpec Output

theorem ProverOutput.ext_iff {ι : Type} {oSpec : OracleSpec ι} {Output PrvState : Type} {x y : ProverOutput oSpec Output PrvState} : x = y ↔ x.output = y.output

theorem ProverOutput.ext {ι : Type} {oSpec : OracleSpec ι} {Output PrvState : Type} {x y : ProverOutput oSpec Output PrvState} (output : x.output = y.output) : x = y

structure ProverInteraction {ι : Type} (oSpec : OracleSpec ι) {n : ℕ} (pSpec : ProtocolSpec n) extends ProverState n, ProverInit (self.PrvState 0), ProverRound oSpec pSpec : Type (max 1 u_1)

The type of algorithms that participates in an (interactive) reduction in the role of the prover. This consists of:

• PrvState 0, ..., PrvState n: the types for the private state, from before the first message to after the last message
• init : PrvState 0 is the initial state
• sendMessage and receiveChallenge are the functions for sending and receiving messages for each round, depending on the direction of the round.

This is useful when modeling soundness, since we do not want to mandate that adversarial provers in the soundness game need to input or output anything.

• PrvState : Fin (n + 1) → Type
• init : self.PrvState 0
• sendMessage (i : pSpec.MessageIdx) : self.PrvState (↑i).castSucc → OracleComp oSpec (pSpec.Message i × self.PrvState (↑i).succ)
• receiveChallenge (i : pSpec.ChallengeIdx) : self.PrvState (↑i).castSucc → OracleComp oSpec (pSpec.Challenge i → self.PrvState (↑i).succ)

structure ProverInteractionWithOutput {ι : Type} (oSpec : OracleSpec ι) (Output : Type) {n : ℕ} (pSpec : ProtocolSpec n) extends ProverState n, ProverInit (self.PrvState 0), ProverRound oSpec pSpec, ProverOutput oSpec Output (self.PrvState (Fin.last n)) : Type (max 1 u_1)

The type of algorithms that participates in an (interactive) reduction in the role of the prover, and returns some specified output type Output. This consists of:

• A ProverInteraction type for the interaction with the verifier
• An output function that takes in the algorithm's final state and returns an oracle computation that outputs the output type Output

This is useful when modeling knowledge soundness, since we do not want to mandate that adversarial provers in the knowledge soundness game need to input the input statement or witness. We also do not need the adversarial prover to output any output statement, as such values are sourced from the verifier.

• PrvState : Fin (n + 1) → Type
• init : self.PrvState 0
• sendMessage (i : pSpec.MessageIdx) : self.PrvState (↑i).castSucc → OracleComp oSpec (pSpec.Message i × self.PrvState (↑i).succ)
• receiveChallenge (i : pSpec.ChallengeIdx) : self.PrvState (↑i).castSucc → OracleComp oSpec (pSpec.Challenge i → self.PrvState (↑i).succ)
• output : self.PrvState (Fin.last n) → OracleComp oSpec Output

structure Prover {ι : Type} (oSpec : OracleSpec ι) (StmtIn WitIn StmtOut WitOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) extends ProverState n, ProverInput StmtIn WitIn (self.PrvState 0), ProverRound oSpec pSpec, ProverOutput oSpec (StmtOut × WitOut) (self.PrvState (Fin.last n)) : Type (max 1 u_1)

The type of honest provers for an interactive reduction with n messages. This consists of:

• PrvState 0, ..., PrvState n are the types for the prover's state at each round
• input initializes the prover's state by taking in the input statement and witness
• sendMessage takes in the prover's state, then returns an oracle computation that outputs a message and the next prover's state
• receiveChallenge takes in the prover's state, then returns an oracle computation that outputs a function that takes in a challenge and returns the next prover's state
• output returns the output statement and witness from the prover's state

Note that the output statement by the prover is present only to facilitate composing honest provers together. For completeness, we will require that the prover's output statement is always equal to the verifier's output statement. For soundness and knowledge soundness, we will use more restricted types of provers (see ProverInteraction and ProverInteractionWithOutput).

• PrvState : Fin (n + 1) → Type
• input : StmtIn × WitIn → self.PrvState 0
• sendMessage (i : pSpec.MessageIdx) : self.PrvState (↑i).castSucc → OracleComp oSpec (pSpec.Message i × self.PrvState (↑i).succ)
• receiveChallenge (i : pSpec.ChallengeIdx) : self.PrvState (↑i).castSucc → OracleComp oSpec (pSpec.Challenge i → self.PrvState (↑i).succ)
• output : self.PrvState (Fin.last n) → OracleComp oSpec (StmtOut × WitOut)

theorem Prover.ext_iff {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} {x y : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec} : x = y ↔ x.PrvState = y.PrvState ∧ x.input ≍ y.input ∧ x.sendMessage ≍ y.sendMessage ∧ x.receiveChallenge ≍ y.receiveChallenge ∧ x.output ≍ y.output

theorem Prover.ext {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} {x y : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec} (PrvState : x.PrvState = y.PrvState) (input : x.input ≍ y.input) (sendMessage : x.sendMessage ≍ y.sendMessage) (receiveChallenge : x.receiveChallenge ≍ y.receiveChallenge) (output : x.output ≍ y.output) : x = y

structure Verifier {ι : Type} (oSpec : OracleSpec ι) (StmtIn StmtOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) : Type u_1

A verifier of an interactive protocol is a function that takes in the input statement and the transcript, and performs an oracle computation that outputs a new statement

• verify : StmtIn → pSpec.FullTranscript → OptionT (OracleComp oSpec) StmtOut

theorem Verifier.ext_iff {ι : Type} {oSpec : OracleSpec ι} {StmtIn StmtOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} {x y : Verifier oSpec StmtIn StmtOut pSpec} : x = y ↔ x.verify = y.verify

theorem Verifier.ext {ι : Type} {oSpec : OracleSpec ι} {StmtIn StmtOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} {x y : Verifier oSpec StmtIn StmtOut pSpec} (verify : x.verify = y.verify) : x = y

@[reducible, inline]

def OracleProver {ι : Type} (oSpec : OracleSpec ι) (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) (WitIn StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) (WitOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) : Type (max 1 u_1)

An (oracle) prover in an interactive oracle reduction is a prover in the non-oracle reduction whose input statement also consists of the underlying messages for the oracle statements

structure OracleVerifier {ι : Type} (oSpec : OracleSpec ι) (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) {n : ℕ} (pSpec : ProtocolSpec n) [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] : Type (max u_1 u_2)

An (oracle) verifier of an interactive oracle reduction consists of:

• an oracle computation verify that outputs the next statement. It may make queries to each of the prover's messages and each of the oracles present in the statement (according to a specified interface defined by OracleInterface instances).

• output oracle statements OStmtOut : ιₛₒ → Type, meant to be a subset of the input oracle statements and the prover's oracle messages. Formally, this is specified by an embedding ιₛₒ ↪ ιₛᵢ ⊕ pSpec.MessageIdx and a proof that OStmtOut is compatible with OStmtIn and pSpec.Messages via this embedding.

Intuitively, the oracle verifier cannot do anything more in returning the output oracle statements, other than specifying a subset of the ones it has received (and dropping the rest).

• verify : StmtIn → pSpec.Challenges → OptionT (OracleComp (oSpec + ([OStmtIn]ₒ + [pSpec.Message]ₒ))) StmtOut

  The core verification logic. Takes the input statement stmtIn and all verifier challenges challenges (which are determined outside this function, typically by sampling for public-coin protocols). Returns the output statement StmtOut within an OracleComp that has access to external oracles oSpec, input statement oracles OStmtIn, and prover message oracles pSpec.Message.

• embed : ιₛₒ ↪ ιₛᵢ ⊕ pSpec.MessageIdx

  An embedding that specifies how each output oracle statement (indexed by ιₛₒ) is derived. It maps an index i : ιₛₒ to either an index j : ιₛᵢ (meaning OStmtOut i comes from OStmtIn j) or an index k : pSpec.MessageIdx (meaning OStmtOut i comes from the prover's message pSpec.Message k). This enforces that output oracles are a subset of input oracles or received prover messages.

• hEq (i : ιₛₒ) : OStmtOut i = match self.embed i with | Sum.inl j => OStmtIn j | Sum.inr j => pSpec.Message j

  A proof term ensuring that the type of each OStmtOut i matches the type of the corresponding source oracle statement (OStmtIn j or pSpec.Message k) as determined by the embed mapping.

theorem OracleVerifier.ext {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {n : ℕ} {pSpec : ProtocolSpec n} {Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)} {Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)} {x y : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec} (verify : x.verify = y.verify) (embed : x.embed = y.embed) : x = y

theorem OracleVerifier.ext_iff {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {n : ℕ} {pSpec : ProtocolSpec n} {Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)} {Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)} {x y : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec} : x = y ↔ x.verify = y.verify ∧ x.embed = y.embed

def OracleVerifier.toVerifier {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {n : ℕ} {pSpec : ProtocolSpec n} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] (verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : Verifier oSpec (StmtIn × ((i : ιₛᵢ) → OStmtIn i)) (StmtOut × ((i : ιₛₒ) → OStmtOut i)) pSpec

An oracle verifier can be seen as a (non-oracle) verifier by providing the oracle interface using its knowledge of the oracle statements and the transcript messages in the clear

def OracleVerifier.numQueries {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {n : ℕ} {pSpec : ProtocolSpec n} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] (stmt : StmtIn) (challenges : (i : pSpec.ChallengeIdx) → pSpec.Challenge i) (verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : OracleComp (oSpec + ([OStmtIn]ₒ + [pSpec.Message]ₒ)) ℕ

The number of queries made to the oracle statements and the prover's messages, for a given input statement and challenges.

This is given as an oracle computation itself, since the oracle verifier may be adaptive and has different number of queries depending on the prior responses.

TODO: define once numQueries is defined in OracleComp

structure OracleVerifier.NonAdaptive {ι : Type} (oSpec : OracleSpec ι) (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) {n : ℕ} (pSpec : ProtocolSpec n) [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] : Type (max (max u_1 u_2) u_3)

A non-adaptive oracle verifier is an oracle verifier that makes a fixed list of queries to the input oracle statements and the prover's messages. These queries can depend on the input statement and the challenges, but later queries are not dependent on the responses of previous queries.

Formally, we model this as a tuple of functions:

• queryOStmt, which outputs a list of queries to the input oracle statements,
• queryMsg, which outputs a list of queries to the prover's messages,
• verify, which outputs the new statement from the query-response pairs.

We allow querying the shared oracle (i.e. probabilistic sampling or random oracles) when deriving the output statement, but not on the list of queries made to the oracle statements or the prover's messages.

Finally, we also allow for choosing a subset of the input oracle statements + the prover's messages to retain for the output oracle statements.

• queryOStmt : StmtIn → ((i : pSpec.ChallengeIdx) → pSpec.Challenge i) → List ((i : ιₛᵢ) × OracleInterface.Query (OStmtIn i))

  Makes a list of queries to each of the oracle statements, given the input statement and the challenges

• queryMsg : StmtIn → ((i : pSpec.ChallengeIdx) → pSpec.Challenge i) → List ((i : pSpec.MessageIdx) × OracleInterface.Query (pSpec.Message i))

  Makes a list of queries to each of the prover's messages, given the input statement and the challenges

• verify : StmtIn → ((i : pSpec.ChallengeIdx) → pSpec.Challenge i) → List ((i : ιₛᵢ) × (q : OracleInterface.Query (OStmtIn i)) × OracleInterface.Response q) → List ((i : pSpec.MessageIdx) × (q : OracleInterface.Query (pSpec.Message i)) × OracleInterface.Response q) → OracleComp oSpec StmtOut

  From the query-response pairs, returns a computation that outputs the new output statement

• embed : ιₛₒ ↪ ιₛᵢ ⊕ pSpec.MessageIdx
• hEq (i : ιₛₒ) : OStmtOut i = match self.embed i with | Sum.inl j => OStmtIn j | Sum.inr j => pSpec.Message j

def OracleVerifier.NonAdaptive.toOracleVerifier {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {n : ℕ} {pSpec : ProtocolSpec n} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] (naVerifier : NonAdaptive oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec

Converts a non-adaptive oracle verifier into the general oracle verifier interface.

This essentially performs the queries via List.mapM, then runs verify on the query-response pairs.

def OracleVerifier.NonAdaptive.numOStmtQueries {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {n : ℕ} {pSpec : ProtocolSpec n} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] [DecidableEq ιₛᵢ] (i : ιₛᵢ) (stmt : StmtIn) (challenges : (i : pSpec.ChallengeIdx) → pSpec.Challenge i) (naVerifier : NonAdaptive oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : ℕ

The number of queries made to the i-th oracle statement, for a given input statement and challenges.

def OracleVerifier.NonAdaptive.numOMsgQueries {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {n : ℕ} {pSpec : ProtocolSpec n} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] (i : pSpec.MessageIdx) (stmt : StmtIn) (challenges : (i : pSpec.ChallengeIdx) → pSpec.Challenge i) (naVerifier : NonAdaptive oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : ℕ

The number of queries made to the i-th prover's message, for a given input statement and challenges.

def OracleVerifier.NonAdaptive.totalNumQueries {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {n : ℕ} {pSpec : ProtocolSpec n} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] (stmt : StmtIn) (challenges : (i : pSpec.ChallengeIdx) → pSpec.Challenge i) (naVerifier : NonAdaptive oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : ℕ

The total number of queries made to the oracle statements and the prover's messages, for a given input statement and challenges.

structure Reduction {ι : Type} (oSpec : OracleSpec ι) (StmtIn WitIn StmtOut WitOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) : Type (max 1 u_1)

An interactive reduction for a given protocol specification pSpec, and relative to oracles defined by oSpec, consists of a prover and a verifier.

• prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec
• verifier : Verifier oSpec StmtIn StmtOut pSpec

theorem Reduction.ext {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} {x y : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec} (prover : x.prover = y.prover) (verifier : x.verifier = y.verifier) : x = y

theorem Reduction.ext_iff {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} {x y : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec} : x = y ↔ x.prover = y.prover ∧ x.verifier = y.verifier

structure OracleReduction {ι : Type} (oSpec : OracleSpec ι) (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) (WitIn StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) (WitOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] : Type (max (max 1 u_1) u_2)

An interactive oracle reduction for a given protocol specification pSpec, and relative to oracles defined by oSpec, consists of a prover and an oracle verifier.

• prover : OracleProver oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec
• verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec

theorem OracleReduction.ext_iff {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {WitIn StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} {Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)} {Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)} {x y : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec} : x = y ↔ x.prover = y.prover ∧ x.verifier = y.verifier

theorem OracleReduction.ext {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {WitIn StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} {Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)} {Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)} {x y : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec} (prover : x.prover = y.prover) (verifier : x.verifier = y.verifier) : x = y

def OracleReduction.toReduction {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {WitIn StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] (oracleReduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec) : Reduction oSpec (StmtIn × ((i : ιₛᵢ) → OStmtIn i)) WitIn (StmtOut × ((i : ιₛₒ) → OStmtOut i)) WitOut pSpec

An interactive oracle reduction can be seen as an interactive reduction, via coercing the oracle verifier to a (normal) verifier

@[reducible]

def Proof {ι : Type} (oSpec : OracleSpec ι) (Statement Witness : Type) {n : ℕ} (pSpec : ProtocolSpec n) : Type (max 1 u_1)

An interactive proof (IP) is an interactive reduction where the output statement is a boolean, the output witness is trivial (a Unit), and the relation checks whether the output statement is true.

@[reducible]

def OracleProof {ι : Type} (oSpec : OracleSpec ι) (Statement : Type) {ιₛᵢ : Type} (OStatement : ιₛᵢ → Type) (Witness : Type) {n : ℕ} (pSpec : ProtocolSpec n) [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStatement i)] [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] : Type (max (max 1 u_1) u_2)

An interactive oracle proof (IOP) is an interactive oracle reduction where the output statement is a boolean, while both the output oracle statement & the output witness are trivial (Unit type).

As a consequence, the output relation in an IOP is effectively a function Bool → Prop, which we can again assume to be the trivial one (sending true to True).

@[reducible]

def NonInteractiveProver (Message : Type) {ι : Type} (oSpec : OracleSpec ι) (StmtIn WitIn StmtOut WitOut : Type) : Type (max 1 u_1)

A non-interactive prover is a prover that only sends a single message to the verifier.

@[reducible]

def NonInteractiveVerifier (Message : Type) {ι : Type} (oSpec : OracleSpec ι) (StmtIn StmtOut : Type) : Type u_1

A non-interactive verifier is a verifier that only receives a single message from the prover.

@[reducible]

def NonInteractiveReduction (Message : Type) {ι : Type} (oSpec : OracleSpec ι) (StmtIn WitIn StmtOut WitOut : Type) : Type (max 1 u_1)

A non-interactive reduction is an interactive reduction with only a single message from the prover to the verifier (and none in the other direction).

def Prover.id {ι : Type} {oSpec : OracleSpec ι} {Statement Witness : Type} : Prover oSpec Statement Witness Statement Witness !p[]

The trivial / identity prover, which does not send any messages to the verifier, and returns its input context (statement & witness) as output.

def Verifier.id {ι : Type} {oSpec : OracleSpec ι} {Statement : Type} : Verifier oSpec Statement Statement !p[]

The trivial / identity verifier, which does not receive any messages from the prover, and returns its input statement as output.

def Reduction.id {ι : Type} {oSpec : OracleSpec ι} {Statement Witness : Type} : Reduction oSpec Statement Witness Statement Witness !p[]

The trivial / identity reduction, which consists of the trivial prover and verifier.

def OracleProver.id {ι : Type} {oSpec : OracleSpec ι} {Statement ιₛ : Type} {OStatement : ιₛ → Type} {Witness : Type} : OracleProver oSpec Statement OStatement Witness Statement OStatement Witness !p[]

The trivial / identity prover in an oracle reduction, which unfolds to the trivial prover for the associated non-oracle reduction.

def OracleVerifier.id {ι : Type} {oSpec : OracleSpec ι} {Statement ιₛ : Type} {OStatement : ιₛ → Type} [Oₛ : (i : ιₛ) → OracleInterface (OStatement i)] : OracleVerifier oSpec Statement OStatement Statement OStatement !p[]

The trivial / identity verifier in an oracle reduction, which receives no messages from the prover, and returns its input statement as output.

def OracleReduction.id {ι : Type} {oSpec : OracleSpec ι} {Statement ιₛ : Type} {OStatement : ιₛ → Type} {Witness : Type} [Oₛ : (i : ιₛ) → OracleInterface (OStatement i)] : OracleReduction oSpec Statement OStatement Witness Statement OStatement Witness !p[]

The trivial / identity oracle reduction, which consists of the trivial oracle prover and verifier.

def Prover.trivial {ι : Type} {oSpec : OracleSpec ι} {Statement Witness : Type} : Prover oSpec Statement Witness Statement Witness !p[]

Alias of Prover.id.

---

The trivial / identity prover, which does not send any messages to the verifier, and returns its input context (statement & witness) as output.

def Verifier.trivial {ι : Type} {oSpec : OracleSpec ι} {Statement : Type} : Verifier oSpec Statement Statement !p[]

Alias of Verifier.id.

---

The trivial / identity verifier, which does not receive any messages from the prover, and returns its input statement as output.

def Reduction.trivial {ι : Type} {oSpec : OracleSpec ι} {Statement Witness : Type} : Reduction oSpec Statement Witness Statement Witness !p[]

Alias of Reduction.id.

---

The trivial / identity reduction, which consists of the trivial prover and verifier.

def OracleProver.trivial {ι : Type} {oSpec : OracleSpec ι} {Statement ιₛ : Type} {OStatement : ιₛ → Type} {Witness : Type} : OracleProver oSpec Statement OStatement Witness Statement OStatement Witness !p[]

Alias of OracleProver.id.

---

The trivial / identity prover in an oracle reduction, which unfolds to the trivial prover for the associated non-oracle reduction.

def OracleVerifier.trivial {ι : Type} {oSpec : OracleSpec ι} {Statement ιₛ : Type} {OStatement : ιₛ → Type} [Oₛ : (i : ιₛ) → OracleInterface (OStatement i)] : OracleVerifier oSpec Statement OStatement Statement OStatement !p[]

Alias of OracleVerifier.id.

---

The trivial / identity verifier in an oracle reduction, which receives no messages from the prover, and returns its input statement as output.

def OracleReduction.trivial {ι : Type} {oSpec : OracleSpec ι} {Statement ιₛ : Type} {OStatement : ιₛ → Type} {Witness : Type} [Oₛ : (i : ιₛ) → OracleInterface (OStatement i)] : OracleReduction oSpec Statement OStatement Witness Statement OStatement Witness !p[]

Alias of OracleReduction.id.

---

The trivial / identity oracle reduction, which consists of the trivial oracle prover and verifier.

@[simp]

theorem OracleVerifier.id_toVerifier {ι : Type} {oSpec : OracleSpec ι} {Statement ιₛ : Type} {OStatement : ιₛ → Type} [Oₛ : (i : ιₛ) → OracleInterface (OStatement i)] : OracleVerifier.id.toVerifier = Verifier.id

@[simp]

theorem OracleReduction.id_toReduction {ι : Type} {oSpec : OracleSpec ι} {Statement ιₛ : Type} {OStatement : ιₛ → Type} {Witness : Type} [Oₛ : (i : ιₛ) → OracleInterface (OStatement i)] : OracleReduction.id.toReduction = Reduction.id

class ProtocolSpec.ProverFirst {n : ℕ} (pSpec : ProtocolSpec n) [NeZero n] : Prop

A protocol specification with the prover speaking first

• prover_first' : pSpec.dir 0 = Direction.P_to_V

class ProtocolSpec.VerifierFirst {n : ℕ} (pSpec : ProtocolSpec n) [NeZero n] : Prop

• verifier_first' : pSpec.dir 0 = Direction.V_to_P

class ProtocolSpec.ProverLast {n : ℕ} (pSpec : ProtocolSpec n) [inst : NeZero n] : Prop

• prover_last' : pSpec.dir ⟨n - 1, ⋯⟩ = Direction.P_to_V

class ProtocolSpec.VerifierLast {n : ℕ} (pSpec : ProtocolSpec n) [NeZero n] : Prop

A protocol specification with the verifier speaking last

• verifier_last' : pSpec.dir ⟨n - 1, ⋯⟩ = Direction.V_to_P

class ProtocolSpec.ProverOnly (pSpec : ProtocolSpec 1) extends pSpec.ProverFirst : Prop

• prover_first' : pSpec.dir 0 = Direction.P_to_V

def ProtocolSpec.NonInteractive (pSpec : ProtocolSpec 1) : Prop

A non-interactive protocol specification with a single message from the prover to the verifier

class ProtocolSpec.VerifierOnly (pSpec : ProtocolSpec 1) extends pSpec.VerifierFirst : Prop

• verifier_first' : pSpec.dir 0 = Direction.V_to_P

@[simp]

theorem ProtocolSpec.prover_first {n : ℕ} (pSpec : ProtocolSpec n) [NeZero n] [h : pSpec.ProverFirst] : pSpec.dir 0 = Direction.P_to_V

@[simp]

theorem ProtocolSpec.verifier_first {n : ℕ} (pSpec : ProtocolSpec n) [NeZero n] [h : pSpec.VerifierFirst] : pSpec.dir 0 = Direction.V_to_P

@[simp]

theorem ProtocolSpec.prover_last {n : ℕ} (pSpec : ProtocolSpec n) [NeZero n] [h : pSpec.ProverLast] : pSpec.dir ⟨n - 1, ⋯⟩ = Direction.P_to_V

@[simp]

theorem ProtocolSpec.verifier_last {n : ℕ} (pSpec : ProtocolSpec n) [NeZero n] [h : pSpec.VerifierLast] : pSpec.dir ⟨n - 1, ⋯⟩ = Direction.V_to_P

instance ProtocolSpec.instProverLastOfProverFirst {pSpec : ProtocolSpec 1} [pSpec.ProverFirst] : pSpec.ProverLast

instance ProtocolSpec.instVerifierLastOfVerifierFirst {pSpec : ProtocolSpec 1} [pSpec.VerifierFirst] : pSpec.VerifierLast

instance ProtocolSpec.instProverFirstOfProverLast {pSpec : ProtocolSpec 1} [h : pSpec.ProverLast] : pSpec.ProverFirst

instance ProtocolSpec.instVerifierFirst {pSpec : ProtocolSpec 1} [h : pSpec.VerifierFirst] : pSpec.VerifierFirst

@[implicit_reducible]

instance ProtocolSpec.instUniqueMessageIdxOfProverFirst {pSpec : ProtocolSpec 1} [pSpec.ProverFirst] : Unique pSpec.MessageIdx

@[implicit_reducible]

instance ProtocolSpec.instUniqueChallengeIdxOfVerifierFirst {pSpec : ProtocolSpec 1} [pSpec.VerifierFirst] : Unique pSpec.ChallengeIdx

instance ProtocolSpec.instIsEmptyChallengeIdxOfProverFirst {pSpec : ProtocolSpec 1} [h : pSpec.ProverFirst] : IsEmpty pSpec.ChallengeIdx

instance ProtocolSpec.instIsEmptyMessageIdxOfVerifierFirst {pSpec : ProtocolSpec 1} [h : pSpec.VerifierFirst] : IsEmpty pSpec.MessageIdx

@[implicit_reducible]

instance ProtocolSpec.instVCVCompatibleChallengeOfProverFirst {pSpec : ProtocolSpec 1} [pSpec.ProverFirst] (i : pSpec.ChallengeIdx) : VCVCompatible (pSpec.Challenge i)

@[implicit_reducible]

instance ProtocolSpec.instOracleInterfaceMessageOfVerifierFirst {pSpec : ProtocolSpec 1} [pSpec.VerifierFirst] (i : pSpec.MessageIdx) : OracleInterface (pSpec.Message i)

@[implicit_reducible]

instance ProtocolSpec.instOracleInterfaceMessageOfProverFirstOfTypeOfNatFinNat {pSpec : ProtocolSpec 1} [pSpec.ProverFirst] [h : OracleInterface (pSpec.Type 0)] (i : pSpec.MessageIdx) : OracleInterface (pSpec.Message i)

@[implicit_reducible]

instance ProtocolSpec.instVCVCompatibleChallengeOfVerifierFirstOfTypeOfNatFinNat {pSpec : ProtocolSpec 1} [pSpec.VerifierFirst] [h : VCVCompatible (pSpec.Type 0)] (i : pSpec.ChallengeIdx) : VCVCompatible (pSpec.Challenge i)

@[simp]

theorem ProtocolSpec.prover_last_of_two (pSpec : ProtocolSpec 2) [pSpec.ProverLast] : pSpec.dir 1 = Direction.P_to_V

@[simp]

theorem ProtocolSpec.verifier_last_of_two (pSpec : ProtocolSpec 2) [pSpec.VerifierLast] : pSpec.dir 1 = Direction.V_to_P

class ProtocolSpec.IsSingleRound (pSpec : ProtocolSpec 2) extends pSpec.ProverFirst, pSpec.VerifierLast : Prop

A protocol specification with a single round of interaction consisting of two messages, with the prover speaking first and the verifier speaking last

This notation is currently somewhat ambiguous, given that there are other valid ways of defining a "single-round" protocol, such as letting the verifier speaks first, letting the prover speaks multiple times, etc.

• prover_first' : pSpec.dir 0 = Direction.P_to_V
• verifier_last' : pSpec.dir ⟨2 - 1, ⋯⟩ = Direction.V_to_P

def ProtocolSpec.ProverThenVerifier (pSpec : ProtocolSpec 2) : Prop

Alias of ProtocolSpec.IsSingleRound.

---

A protocol specification with a single round of interaction consisting of two messages, with the prover speaking first and the verifier speaking last

This notation is currently somewhat ambiguous, given that there are other valid ways of defining a "single-round" protocol, such as letting the verifier speaks first, letting the prover speaks multiple times, etc.

@[implicit_reducible]

instance ProtocolSpec.IsSingleRound.instUniqueMessageIdx {pSpec : ProtocolSpec 2} [pSpec.IsSingleRound] : Unique pSpec.MessageIdx

The first message is the only message from the prover to the verifier

@[implicit_reducible]

instance ProtocolSpec.IsSingleRound.instUniqueChallengeIdx {pSpec : ProtocolSpec 2} [pSpec.IsSingleRound] : Unique pSpec.ChallengeIdx

The second message is the only challenge from the verifier to the prover

@[implicit_reducible]

instance ProtocolSpec.IsSingleRound.instOracleInterfaceMessageOfDefaultMessageIdx {pSpec : ProtocolSpec 2} [pSpec.IsSingleRound] [h : OracleInterface (pSpec.Message default)] (i : pSpec.MessageIdx) : OracleInterface (pSpec.Message i)

@[implicit_reducible]

instance ProtocolSpec.IsSingleRound.instVCVCompatibleChallengeOfDefaultChallengeIdx {pSpec : ProtocolSpec 2} [pSpec.IsSingleRound] [h : VCVCompatible (pSpec.Challenge default)] (i : pSpec.ChallengeIdx) : VCVCompatible (pSpec.Challenge i)

@[reducible, inline]

def ProtocolSpec.FullTranscript.mk2 {pSpec : ProtocolSpec 2} (msg0 : pSpec.Type 0) (msg1 : pSpec.Type 1) : pSpec.FullTranscript

theorem ProtocolSpec.FullTranscript.mk2_eq_snoc_snoc {pSpec : ProtocolSpec 2} (msg0 : pSpec.Type 0) (msg1 : pSpec.Type 1) : mk2 msg0 msg1 = Transcript.concat msg1 (Transcript.concat msg0 default)

class Prover.IsPure {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (P : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) : Prop

• is_pure : ∃ (sendMessage : (x : pSpec.MessageIdx) → P.PrvState (↑x).castSucc → pSpec.Message x × P.PrvState (↑x).succ), ∀ (i : pSpec.MessageIdx) (st : P.PrvState (↑i).castSucc), P.sendMessage i st = pure (sendMessage i st)

class Verifier.IsPure {ι : Type} {oSpec : OracleSpec ι} {StmtIn StmtOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (V : Verifier oSpec StmtIn StmtOut pSpec) : Prop

• is_pure : ∃ (verify : StmtIn → pSpec.FullTranscript → StmtOut), ∀ (stmtIn : StmtIn) (transcript : pSpec.FullTranscript), V.verify stmtIn transcript = pure (verify stmtIn transcript)

class Reduction.IsPure {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (R : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec) : Prop

• prover_is_pure : R.prover.IsPure
• verifier_is_pure : R.verifier.IsPure