An oracle interface for an underlying data type \(\mathsf{D}\) consists of the following:

• A type \(\mathsf{Q}\) for queries to the oracle,

• A type \(\mathsf{R}\) for responses from the oracle,

• A function \(\mathsf{oracle} : \mathsf{D} \to \mathsf{Q} \to \mathsf{R}\) that specifies the oracle’s behavior given the underlying data and a query.

In an (oracle) reduction, its (oracle) context consists of a statement type, a witness type, and (in the oracle case) an indexed list of oracle statement types.

Currently, we do not abstract out / bundle the context as a separate structure, but rather specifies the types explicitly. This may change in the future.

A protocol specification for an \(n\)-message (oracle) reduction, is an element of the following type:

ProtocolSpec n := Fin n Direction×Type. In the above, \(\mathsf{Direction}:= \{ \mathsf{P \! \! \rightarrow \! \! V}, \mathsf{V \! \! \rightarrow \! \! P}\} \) is the type of possible directions of messages, and \(\mathsf{Fin}\ n := \{ i : \mathbb {N}\mathbin {/\! /}i {\lt} n \} \) is the type of all natural numbers less than \(n\).

In other words, for each step \(i\) of interaction, the protocol specification describes the direction of the message sent in that step, i.e., whether it is from the prover or from the verifier. It also describes the type of that message.

In the oracle setting, we also expect an oracle interface for each message from the prover to the verifier.

Given a protocol spec \(\mathsf{pSpec}: \mathsf{ProtocolSpec}\ n\), we define:

• \(\mathsf{pSpec}.\mathsf{Dir}\ i := (\mathsf{pSpec}\ i).\mathsf{fst}\) extracts the direction of the \(i\)-th message.

• \(\mathsf{pSpec}.\mathsf{Type}\ i := (\mathsf{pSpec}\ i).\mathsf{snd}\) extracts the type of the \(i\)-th message.

• \(\mathsf{pSpec}.\mathsf{MessageIdx}:= \{ i : \mathsf{Fin}\ n \mathbin {/\! /}\mathsf{pSpec}.\mathsf{Dir}\ i = \mathsf{P \! \! \rightarrow \! \! V}\} \) is the subtype of indices corresponding to prover messages.

• \(\mathsf{pSpec}.\mathsf{ChallengeIdx}:= \{ i : \mathsf{Fin}\ n \mathbin {/\! /}\mathsf{pSpec}.\mathsf{Dir}\ i = \mathsf{V \! \! \rightarrow \! \! P}\} \) is the subtype of indices corresponding to verifier challenges.

• \(\mathsf{pSpec}.\mathsf{Message}\ i := (i : \mathsf{pSpec}.\mathsf{MessageIdx}) \to \mathsf{pSpec}.\mathsf{Type}\ i.\mathsf{val}\) is an indexed family of message types in the protocol.

• \(\mathsf{pSpec}.\mathsf{Challenge}\ i := (i : \mathsf{pSpec}.\mathsf{ChallengeIdx}) \to \mathsf{pSpec}.\mathsf{Type}\ i.\mathsf{val}\) is an indexed family of challenge types in the protocol.

Given protocol specification \(\mathsf{pSpec}: \mathsf{ProtocolSpec}\ n\), we define:

• A transcript up to round \(k : \mathsf{Fin}\ (n + 1)\) is an element of type

  \[ \mathsf{Transcript}\ k\ \mathsf{pSpec}:= (i : \mathsf{Fin}\ k) \to \mathsf{pSpec}.\mathsf{Type}\ (\uparrow i : \mathsf{Fin}\ n) \]

  where \(\uparrow i : \mathsf{Fin}\ n\) denotes casting \(i : \mathsf{Fin}\ k\) to \(\mathsf{Fin}\ n\) (valid since \(k \leq n + 1\)).

• A full transcript is \(\mathsf{FullTranscript}\ \mathsf{pSpec}:= (i : \mathsf{Fin}\ n) \to \mathsf{pSpec}.\mathsf{Type}\ i\).

• The type of all messages from prover to verifier is

  \[ \mathsf{pSpec}.\mathsf{Messages}:= \prod _{i : \mathsf{pSpec}.\mathsf{MessageIdx}} \mathsf{pSpec}.\mathsf{Message}\ i \]

• The type of all challenges from verifier to prover is

  \[ \mathsf{pSpec}.\mathsf{Challenges}:= \prod _{i : \mathsf{pSpec}.\mathsf{ChallengeIdx}} \mathsf{pSpec}.\mathsf{Challenge}\ i \]

A prover \(\mathcal{P}\) in a reduction consists of the following components:

• Prover State: A family of types \(\mathsf{PrvState} : \mathsf{Fin}(n+1) \to \mathsf{Type}\) representing the prover’s internal state at each round of the protocol.

• Input Processing: A function

  \[ \mathsf{input} : \mathsf{StmtIn}\to \mathsf{WitIn}\to \mathsf{PrvState}(0) \]

  that initializes the prover’s state from the input statement and witness.

• Message Sending: For each message index \(i : \mathsf{pSpec}.\mathsf{MessageIdx}\), a function

  \[ \mathsf{sendMessage}_i : \mathsf{PrvState}(i.\mathsf{val}.\mathsf{castSucc}) \to \mathsf{OracleComp}(\mathsf{oSpec}, \mathsf{pSpec}.\mathsf{Message}(i) \times \mathsf{PrvState}(i.\mathsf{val}.\mathsf{succ})) \]

  that generates the message and updates the prover’s state.

• Challenge Processing: For each challenge index \(i : \mathsf{pSpec}.\mathsf{ChallengeIdx}\), a function

  \[ \mathsf{receiveChallenge}_i : \mathsf{PrvState}(i.\mathsf{val}.\mathsf{castSucc}) \to \mathsf{pSpec}.\mathsf{Challenge}(i) \to \mathsf{PrvState}(i.\mathsf{val}.\mathsf{succ}) \]

  that updates the prover’s state upon receiving a challenge.

• Output Generation: A function

  \[ \mathsf{output} : \mathsf{PrvState}(\mathsf{Fin}.\mathsf{last}(n)) \to \mathsf{StmtOut}\times \mathsf{WitOut} \]

  that produces the final output statement and witness from the prover’s final state.

An oracle prover is a prover whose input statement includes the underlying data for oracle statements, and whose output includes oracle statements. Formally, it is a prover with input statement type \(\mathsf{StmtIn}\times (\forall i : \iota _{\mathsf{si}}, \mathsf{OStmtIn}(i))\) and output statement type \(\mathsf{StmtOut}\times (\forall i : \iota _{\mathsf{so}}, \mathsf{OStmtOut}(i))\), where:

• \(\mathsf{OStmtIn}: \iota _{\mathsf{si}} \to \mathsf{Type}\) are the input oracle statement types

• \(\mathsf{OStmtOut}: \iota _{\mathsf{so}} \to \mathsf{Type}\) are the output oracle statement types

A verifier \(\mathcal{V}\) in a reduction is specified by a single function:

This function takes the input statement and the complete transcript of the protocol interaction, and performs an oracle computation (potentially querying the shared oracle \(\mathsf{oSpec}\)) to produce an output statement.

The verifier is assumed to be public-coin, meaning it only sends uniformly random challenges and uses no other randomness beyond what is provided by the shared oracle.

An oracle verifier \(\mathcal{V}\) consists of the following components:

• Verification Logic: A function

  \[ \mathsf{verify} : \mathsf{StmtIn}\to \mathsf{pSpec}.\mathsf{Challenges}\to \mathsf{OracleComp}(\mathsf{oSpec}\mathrel {++_\mathsf {o}} ([\mathsf{OStmtIn}]_\mathsf {o} \mathrel {++_\mathsf {o}} [\mathsf{pSpec}.\mathsf{Message}]_\mathsf {o}), \mathsf{StmtOut}) \]

  that takes the input statement and verifier challenges, and performs oracle queries to the shared oracle, input oracle statements, and prover messages to produce an output statement.

• Output Oracle Embedding: An injective function

  \[ \mathsf{embed} : \iota _{\mathsf{so}} \hookrightarrow \iota _{\mathsf{si}} \oplus \mathsf{pSpec}.\mathsf{MessageIdx} \]

  that specifies how each output oracle statement is derived from either an input oracle statement or a prover message.

• Type Compatibility: A proof term

  \[ \mathsf{hEq} : \forall i : \iota _{\mathsf{so}}, \mathsf{OStmtOut}(i) = \begin{cases} \end{cases} \mathsf{OStmtIn}(j) & \text{if } \mathsf{embed}(i) = \mathsf{inl}(j) \\ \mathsf{pSpec}.\mathsf{Message}(k) & \text{if } \mathsf{embed}(i) = \mathsf{inr}(k) \end{cases} \]

  ensuring that output oracle statement types match their sources.

This design ensures that output oracle statements are always a subset of the available input oracle statements and prover messages.

An oracle verifier can be converted to a standard verifier through a natural simulation process. The key insight is that while an oracle verifier only has oracle access to certain data (input oracle statements and prover messages), a standard verifier can be given the actual underlying data directly.

The conversion works as follows: when the oracle verifier needs to make an oracle query to some data, the converted verifier can respond to this query immediately using the actual underlying data it possesses. This is accomplished through the OracleInterface type class, which specifies for each data type how to respond to queries given the underlying data.

Specifically, given an oracle verifier \(\mathcal{V}_{\text{oracle}}\):

• The converted verifier \(\mathcal{V}_{\text{oracle}}.\mathsf{toVerifier}\) takes as input both the statement and the actual underlying data for all oracle statements

• When \(\mathcal{V}_{\text{oracle}}\) attempts to query an oracle statement or prover message, the converted verifier uses the corresponding OracleInterface instance to compute the response from the actual data

• The output oracle statements are constructed according to the embedding specification, selecting the appropriate subset of input oracle statements and prover messages

An interactive reduction for protocol specification \(\mathsf{pSpec}: \mathsf{ProtocolSpec}(n)\) and oracle specification \(\mathsf{oSpec}\) consists of:

• A prover \(\mathcal{P} : \mathsf{Prover}(\mathsf{pSpec}, \mathsf{oSpec}, \mathsf{StmtIn}, \mathsf{WitIn}, \mathsf{StmtOut}, \mathsf{WitOut})\)

• A verifier \(\mathcal{V} : \mathsf{Verifier}(\mathsf{pSpec}, \mathsf{oSpec}, \mathsf{StmtIn}, \mathsf{StmtOut})\)

The reduction establishes a relationship between input relations on \((\mathsf{StmtIn}, \mathsf{WitIn})\) and output relations on \((\mathsf{StmtOut}, \mathsf{WitOut})\) through the interactive protocol defined by \(\mathsf{pSpec}\).

An interactive oracle reduction for protocol specification \(\mathsf{pSpec}: \mathsf{ProtocolSpec}(n)\) with oracle interfaces for all prover messages, and oracle specification \(\mathsf{oSpec}\), consists of:

• An oracle prover \(\mathcal{P} : \mathsf{OracleProver}(\mathsf{pSpec}, \mathsf{oSpec}, \mathsf{StmtIn}, \mathsf{WitIn}, \mathsf{StmtOut}, \mathsf{WitOut}, \mathsf{OStmtIn}, \mathsf{OStmtOut})\)

• An oracle verifier \(\mathcal{V} : \mathsf{OracleVerifier}(\mathsf{pSpec}, \mathsf{oSpec}, \mathsf{StmtIn}, \mathsf{StmtOut}, \mathsf{OStmtIn}, \mathsf{OStmtOut})\)

where:

• \(\mathsf{OStmtIn}: \iota _{\mathsf{si}} \to \mathsf{Type}\) are the input oracle statement types with oracle interfaces

• \(\mathsf{OStmtOut}: \iota _{\mathsf{so}} \to \mathsf{Type}\) are the output oracle statement types

The oracle reduction allows the verifier to access prover messages and oracle statements only through specified oracle interfaces, enabling more flexible and composable protocol designs.

The execution of a prover up to round \(i : \mathsf{Fin}(n+1)\) is defined inductively:

where \(\mathsf{processRound}\) handles individual rounds by either:

• Verifier Challenge (\(\mathsf{pSpec}.\mathsf{getDir}(j) = \mathsf{V\_ to\_ P}\)): Query for a challenge and update prover state

• Prover Message (\(\mathsf{pSpec}.\mathsf{getDir}(j) = \mathsf{P\_ to\_ V}\)): Generate message via \(\mathsf{sendMessage}\) and update state

Returns the transcript up to round \(i\) and the prover’s state after round \(i\).

The complete execution of a prover is defined as:

Returns the output statement, output witness, and complete transcript.

The execution of a verifier is simply the application of its verification function:

This takes the input statement and full transcript, and returns the output statement via an oracle computation.

The execution of an oracle verifier is defined as:

This simulates the oracle access to input oracle statements and prover messages, then executes the verification logic.

The execution of an interactive reduction consists of running the prover followed by the verifier:

Returns both the prover’s output (statement and witness) and the verifier’s output statement, along with the complete transcript.

The execution of an interactive oracle reduction is similar to a standard reduction but includes logging of oracle queries:

Returns the same outputs as a standard reduction, plus logs of all oracle queries made by both the prover and verifier.

A reduction satisfies completeness with error \(\epsilon \geq 0\) and with respect to input relation \(R_{\text{in}}\) and output relation \(R_{\text{out}}\), if for all valid statement-witness pair \((x_{\text{in}}, w_{\text{in}})\) for \(R_{\text{in}}\), the execution between the honest prover and the honest verifier will result in a tuple \(((x_{\text{out}}^P, w_{\text{out}}), x_{\text{out}}^V)\) such that:

• \(R_{\text{out}}(x_{\text{out}}^V, w_{\text{out}}) = \text{True}\) (the output statement-witness pair is valid), and

• \(x_{\text{out}}^P = x_{\text{out}}^V\) (the output statements are the same from both prover and verifier)

except with probability \(\epsilon \).

A reduction satisfies perfect completeness if it satisfies completeness with error \(0\). This means that the probability of the reduction outputting a valid statement-witness pair is exactly 1 (instead of at least \(1 - 0\)).

A straightline, deterministic, non-oracle-querying extractor takes in:

• the output witness \(w_{\text{out}}\),

• the initial statement \(x_{\text{in}}\),

• the IOR transcript \(\tau \),

• the query logs from the prover and verifier

and returns a corresponding initial witness \(w_{\text{in}}\).

Note that the extractor does not need to take in the output statement, since it can be derived via re-running the verifier on the initial statement, the transcript, and the verifier’s query log.

This form of extractor suffices for proving knowledge soundness of most hash-based IOPs.

A round-by-round extractor with index \(m\) is given:

• the input statement \(x_{\text{in}}\),

• a partial transcript of length \(m\),

• the prover’s query log

and returns a witness to the statement.

Note that the RBR extractor does not need to take in the output statement or witness.

A rewinding extractor consists of:

• An extractor state type

• Simulation oracles for challenges and oracle queries for the prover

• A function that runs the extractor with the prover’s oracle interface, allowing for calling the prover multiple times

This allows the extractor to rewind the prover to earlier states and try different challenges.

An adaptive prover extends the basic prover type with the ability to choose the input statement adaptively based on oracle access. This models stronger adversaries that can choose their statements after seeing some oracle responses.

A state-restoration prover is a modified prover that has query access to challenge oracles that can return the \(i\)-th challenge, for all \(i\), given the input statement and the transcript up to that point.

It takes in the input statement and witness, and outputs a full transcript of interaction, along with the output statement and witness.

This models adversaries in the state-restoration setting where challenges can be queried programmably.

A reduction satisfies soundness with error \(\epsilon \geq 0\) and with respect to input language \(L_{\text{in}} \subseteq \text{Statement}_{\text{in}}\) and output language \(L_{\text{out}} \subseteq \text{Statement}_{\text{out}}\) if:

• for all (malicious) provers with arbitrary types for witness types,

• for all arbitrary input witness,

• for all input statement \(x_{\text{in}} \notin L_{\text{in}}\),

the execution between the prover and the honest verifier will result in an output statement \(x_{\text{out}} \in L_{\text{out}}\) with probability at most \(\epsilon \).

A reduction satisfies (straightline) knowledge soundness with error \(\epsilon \geq 0\) and with respect to input relation \(R_{\text{in}}\) and output relation \(R_{\text{out}}\) if:

• there exists a straightline extractor \(E\), such that

• for all input statement \(x_{\text{in}}\), witness \(w_{\text{in}}\), and (malicious) prover,

• if the execution with the honest verifier results in a pair \((x_{\text{out}}, w_{\text{out}})\),

• and the extractor produces some \(w'_{\text{in}}\),

then the probability that \((x_{\text{in}}, w'_{\text{in}})\) is not valid for \(R_{\text{in}}\) and yet \((x_{\text{out}}, w_{\text{out}})\) is valid for \(R_{\text{out}}\) is at most \(\epsilon \).

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.

A (deterministic) state function for a verifier, with respect to input language \(L_{\text{in}}\) and output language \(L_{\text{out}}\), consists of a function that maps partial transcripts to boolean values, satisfying:

• For all input statements not in the language, the state function is false for the empty transcript

• If the state function is false for a partial transcript, and the next message is from the prover to the verifier, then the state function is also false for the new partial transcript regardless of the message

• If the state function is false for a full transcript, the verifier will not output a statement in the output language

A knowledge state function for a verifier, with respect to input relation \(R_{\text{in}}\), output relation \(R_{\text{out}}\), and intermediate witness types, extends the basic state function to track witness validity throughout the protocol execution. This is used to define round-by-round knowledge soundness.

A protocol with verifier \(\mathcal{V}\) satisfies round-by-round soundness with respect to input language \(L_{\text{in}}\), output language \(L_{\text{out}}\), and error function \(\epsilon : \text{ChallengeIdx} \to \mathbb {R}_{\geq 0}\) if:

• there exists a state function for the verifier and the input/output languages, such that

• for all initial statements \(x_{\text{in}} \notin L_{\text{in}}\),

• for all initial witnesses,

• for all provers,

• for all challenge rounds \(i\),

the probability that:

• the state function is false for the partial transcript output by the prover

• the state function is true for the partial transcript appended by next challenge (chosen randomly)

is at most \(\epsilon (i)\).

A protocol with verifier \(\mathcal{V}\) satisfies round-by-round knowledge soundness with respect to input relation \(R_{\text{in}}\), output relation \(R_{\text{out}}\), and error function \(\epsilon : \text{ChallengeIdx} \to \mathbb {R}_{\geq 0}\) if:

• there exists a knowledge state function for the verifier and the languages of the input/output relations,

• there exists a round-by-round extractor,

• for all initial statements,

• for all initial witnesses,

• for all provers,

• for all challenge rounds \(i\),

the probability that:

• the extracted witness does not satisfy the input relation

• the state function is false for the partial transcript output by the prover

• the state function is true for the partial transcript appended by next challenge (chosen randomly)

is at most \(\epsilon (i)\).

An extractor is monotone if its success probability on a given query log is the same as the success probability on any extension of that query log. This property ensures that the extractor’s performance does not degrade when given more information.

A round-by-round extractor is monotone if its success probability on a given query log is the same as the success probability on any extension of that query log.

A simulator consists of:

• Oracle simulation capabilities for the shared oracles

• A prover simulation function that takes an input statement and produces a transcript

The simulator should have programming access to the shared oracles and be able to generate transcripts that are indistinguishable from real protocol executions.

Completeness of an oracle reduction is the same as for non-oracle reductions, but applied to the converted reduction where oracle statements are handled through their interfaces.

Soundness of an oracle verifier is defined by converting it to a standard verifier and applying the standard soundness definition.

Knowledge soundness of an oracle verifier is defined by converting it to a standard verifier and applying the standard knowledge soundness definition.

Round-by-round soundness of an oracle verifier is defined by converting it to a standard verifier and applying the standard round-by-round soundness definition.

Round-by-round knowledge soundness of an oracle verifier is defined by converting it to a standard verifier and applying the standard round-by-round knowledge soundness definition.

State-restoration soundness is a security notion where the adversarial prover has access to challenge oracles that can return the \(i\)-th challenge for any round \(i\), given the input statement and the transcript up to that point. This models stronger adversaries in the programmable random oracle model or when challenges can be computed deterministically.

A verifier satisfies state-restoration soundness if for all input statements not in the language, for all witnesses, and for all state-restoration provers, the probability that the verifier outputs a statement in the output language is bounded by the soundness error.

Note: This definition is currently under development in the Lean formalization.

State-restoration knowledge soundness extends state-restoration soundness with the requirement that there exists a straightline extractor that can recover valid witnesses from any state-restoration prover that convinces the verifier.

Note: This definition is currently under development in the Lean formalization.

Given two protocol specifications \(\mathsf{pSpec}_1 : \mathsf{ProtocolSpec}\ m\) and \(\mathsf{pSpec}_2 : \mathsf{ProtocolSpec}\ n\), their sequential composition is:

Given full transcripts \(T_1 : \mathsf{FullTranscript}\ \mathsf{pSpec}_1\) and \(T_2 : \mathsf{FullTranscript}\ \mathsf{pSpec}_2\), their sequential composition is:

Given provers \(P_1 : \mathsf{Prover}\ \mathsf{pSpec}_1\ \mathsf{oSpec}\ \mathsf{StmtIn}_1\ \mathsf{WitIn}_1\ \mathsf{StmtOut}_1\ \mathsf{WitOut}_1\) and \(P_2 : \mathsf{Prover}\ \mathsf{pSpec}_2\ \mathsf{oSpec}\ \mathsf{StmtOut}_1\ \mathsf{WitOut}_1\ \mathsf{StmtOut}_2\ \mathsf{WitOut}_2\), their sequential composition is:

The composed prover works by:

• Running \(P_1\) on the input context to produce an intermediate context

• Using this intermediate context as input to \(P_2\)

• Outputting the final context from \(P_2\)

Given verifiers \(V_1 : \mathsf{Verifier}\ \mathsf{pSpec}_1\ \mathsf{oSpec}\ \mathsf{StmtIn}_1\ \mathsf{StmtOut}_1\) and \(V_2 : \mathsf{Verifier}\ \mathsf{pSpec}_2\ \mathsf{oSpec}\ \mathsf{StmtOut}_1\ \mathsf{StmtOut}_2\), their sequential composition is:

The composed verifier first runs \(V_1\) on the first part of the transcript, then runs \(V_2\) on the second part using the intermediate statement from \(V_1\).

Sequential composition of reductions combines the corresponding provers and verifiers:

Sequential composition extends naturally to oracle reductions by composing the oracle provers and oracle verifiers.

Given a family of protocol specifications \(\mathsf{pSpec}: \forall i : \mathsf{Fin}(m+1), \mathsf{ProtocolSpec}\ (n\ i)\), their composition is:

A statement lens between outer context types \((\mathsf{StmtIn}_{\mathsf{outer}}, \mathsf{StmtOut}_{\mathsf{outer}})\) and inner context types \((\mathsf{StmtIn}_{\mathsf{inner}}, \mathsf{StmtOut}_{\mathsf{inner}})\) consists of:

• \(\mathsf{projStmt}: \mathsf{StmtIn}_{\mathsf{outer}} \to \mathsf{StmtIn}_{\mathsf{inner}}\) (projection to inner context)

• \(\mathsf{liftStmt}: \mathsf{StmtIn}_{\mathsf{outer}} \times \mathsf{StmtOut}_{\mathsf{inner}} \to \mathsf{StmtOut}_{\mathsf{outer}}\) (lifting back to outer context)

A witness lens between outer witness types \((\mathsf{WitIn}_{\mathsf{outer}}, \mathsf{WitOut}_{\mathsf{outer}})\) and inner witness types \((\mathsf{WitIn}_{\mathsf{inner}}, \mathsf{WitOut}_{\mathsf{inner}})\) consists of:

• \(\mathsf{projWit}: \mathsf{WitIn}_{\mathsf{outer}} \to \mathsf{WitIn}_{\mathsf{inner}}\) (projection to inner context)

• \(\mathsf{liftWit}: \mathsf{WitIn}_{\mathsf{outer}} \times \mathsf{WitOut}_{\mathsf{inner}} \to \mathsf{WitOut}_{\mathsf{outer}}\) (lifting back to outer context)

A context lens combines a statement lens and a witness lens for adapting complete reduction contexts.

For oracle reductions, we additionally need lenses for oracle statements that can simulate oracle access between contexts.

Given a prover \(P\) for the inner context and a context lens, the lifted prover works by:

• Projecting the outer input to the inner context

• Running the inner prover

• Lifting the output back to the outer context

A context lens preserves completeness if it maintains relation satisfaction under projection and lifting.

A statement lens preserves soundness if it maps invalid statements to invalid statements.

For round-by-round soundness, we need a slightly relaxed soundness condition.

A context lens preserves knowledge soundness if it maintains witness extractability.

For a protocol specification \(\mathsf{pSpec}\) and input statement type \(\mathsf{StmtIn}\), the Fiat-Shamir challenge oracle interface for the \(i\)-th challenge is defined as follows:

• Query type: \(\mathsf{StmtIn}\times \mathsf{pSpec}.\mathsf{MessagesUpTo}\; i.\mathsf{val}.\mathsf{castSucc}\)

• Response type: \(\mathsf{pSpec}.\mathsf{Challenge}\; i\)

• Oracle behavior: Returns the challenge (which is determined by the random oracle)

The query consists of the input statement and all prover messages sent up to (but not including) round \(i\).

The Fiat-Shamir oracle specification for a protocol \(\mathsf{pSpec}\) with input statement type \(\mathsf{StmtIn}\) is:

where for each challenge index \(i\), the oracle domain is \(\mathsf{StmtIn}\times \mathsf{pSpec}.\mathsf{MessagesUpTo}\; i.\mathsf{val}.\mathsf{castSucc}\) and the range is \(\mathsf{pSpec}.\mathsf{Challenge}\; i\).

This specification defines a family of oracles, one for each challenge round, that deterministically computes challenges based on the statement and messages up to that round.

The modified round processing function for Fiat-Shamir maintains the prover messages (but not challenges) and the input statement throughout execution:

For each round \(j\):

• If \(j\) is a challenge round: Query the Fiat-Shamir oracle with the statement and messages so far, then update the prover state with the received challenge

• If \(j\) is a message round: Generate the message using the prover’s \(\mathsf{sendMessage}\) function and append it to the message history

The key difference from standard execution is that challenges are derived via oracle queries rather than received from an interactive verifier.

The Fiat-Shamir prover execution up to round \(i\) is defined as:

This executes the prover inductively using \(\mathsf{processRoundFS}\), starting from the initial state and accumulating messages and the statement. Returns the messages up to round \(i\), the input statement, and the prover’s final state.

Given an interactive prover \(P\) for protocol \(\mathsf{pSpec}\), the Fiat-Shamir transformation produces a non-interactive prover:

The transformed prover:

• Has state type that combines the statement with the original prover’s state at round 0, and uses the final state type for subsequent rounds

• On input, stores both the statement and initializes the original prover’s state

• Sends a single message containing all of the original prover’s messages, computed via \(\mathsf{runToRoundFS}\)

• Never receives challenges (since it’s non-interactive)

• Outputs using the original prover’s output function

Given a collection of prover messages and an input statement, the function \(\mathsf{deriveTranscriptFS}\) reconstructs the full protocol transcript up to round \(k\):

This is computed inductively:

• For challenge rounds: Query the Fiat-Shamir oracle with the statement and messages up to that point

• For message rounds: Use the corresponding message from the prover

The result is a complete transcript that includes both prover messages and verifier challenges.

Given an interactive verifier \(V\) for protocol \(\mathsf{pSpec}\), the Fiat-Shamir transformation produces a non-interactive verifier:

The transformed verifier:

• Takes the input statement and a proof consisting of all prover messages

• Derives the full transcript using \(\mathsf{deriveTranscriptFS}\)

• Runs the original verifier’s verification logic on the reconstructed transcript

Given an interactive reduction \(R\) for protocol \(\mathsf{pSpec}\), the Fiat-Shamir transformation produces a non-interactive reduction:

This transformation simply applies the Fiat-Shamir transformation to both the prover and verifier components of the reduction.