Execution Semantics of Interactive Oracle Reductions

We define what it means to execute an interactive oracle reduction, and prove some basic properties.

@[simp]

theorem loggingOracle.impl_run {ι : Type u} {spec : OracleSpec ι} {i : ι} {t : spec.domain i} : (loggingOracle.impl (OracleSpec.query i t)).run = do let u ← liftM (OracleSpec.query i t) pure (u, [⟨i, (t, u)⟩])

@[simp]

theorem loggingOracle.simulateQ_map_fst {ι : Type u} {spec : OracleSpec ι} {α : Type u} (oa : OracleComp spec α) : Prod.fst <$> (OracleComp.simulateQ loggingOracle oa).run = oa

@[simp]

theorem loggingOracle.simulateQ_bind_fst {ι : Type u} {spec : OracleSpec ι} {α β : Type u} (oa : OracleComp spec α) (f : α → OracleComp spec β) : (do let a ← (OracleComp.simulateQ loggingOracle oa).run f a.1) = oa >>= f

theorem loggingOracle.simulateQ_bind_fst_comp {ι : Type u} {spec : OracleSpec ι} {α β : Type u} (oa : OracleComp spec α) (f : α → OracleComp spec β) : (do let a ← (OracleComp.simulateQ loggingOracle oa).run f a.1) = do let a ← oa f a

We often have to specify oa and f for this to be applied

@[simp]

theorem loggingOracle.simulateQ_run_liftComp_fst {ι : Type u} {spec : OracleSpec ι} {α ι' : Type u} {superSpec : OracleSpec ι'} (oa : OracleComp spec α) [spec ⊂ₒ superSpec] : Prod.fst <$> (OracleComp.simulateQ loggingOracle oa).run.liftComp superSpec = Prod.fst <$> (OracleComp.simulateQ loggingOracle (oa.liftComp superSpec)).run

Ideally, this theorem can also compare the logs of the two oracle computations.

For this to work, we need an extra function mapping superSpec.QueryLog to spec.QueryLog.

This function always exists if superSpec is spec ++ₒ something, and extensions thereof, but may not be guaranteed to exist in general, if we just have the current fields in the type class.

@[inline, specialize #[]]

def Prover.processRound {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (j : Fin n) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) (currentResult : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) (ProtocolSpec.Transcript j.castSucc pSpec × prover.PrvState j.castSucc)) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) (ProtocolSpec.Transcript j.succ pSpec × prover.PrvState j.succ)

Prover's function for processing the next round, given the current result of the previous round, and a function for getting the challenge.

Equations

• One or more equations did not get rendered due to their size.

@[inline, specialize #[]]

def Prover.runToRound {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (i : Fin (n + 1)) (stmt : StmtIn) (wit : WitIn) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) (ProtocolSpec.Transcript i pSpec × prover.PrvState i)

Run the prover in an interactive reduction up to round index i, via first inputting the statement and witness, and then processing each round up to round i. Returns the transcript up to round i, and the prover's state after round i.

Equations

• Prover.runToRound i stmt wit prover = Fin.induction (pure (default, prover.input (stmt, wit))) (fun (j : Fin n) => Prover.processRound j prover) i

@[inline, specialize #[]]

def Prover.runWithLogToRound {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (i : Fin (n + 1)) (stmt : StmtIn) (wit : WitIn) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) ((ProtocolSpec.Transcript i pSpec × prover.PrvState i) × (oSpec ++ₒ [pSpec.Challenge]ₒ).QueryLog)

Run the prover in an interactive reduction up to round i, logging all the queries made by the prover. Returns the transcript up to that round, the prover's state after that round, and the log of the prover's oracle queries. This basically just wraps runToRound with a logging oracle.

Equations

• Prover.runWithLogToRound i stmt wit prover = (OracleComp.simulateQ loggingOracle (Prover.runToRound i stmt wit prover)).run

@[simp]

theorem Prover.runWithLogToRound_discard_log_eq_runToRound {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (i : Fin (n + 1)) (stmt : StmtIn) (wit : WitIn) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) : Prod.fst <$> runWithLogToRound i stmt wit prover = runToRound i stmt wit prover

@[inline, specialize #[]]

def Prover.run {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (stmt : StmtIn) (wit : WitIn) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) (pSpec.FullTranscript × StmtOut × WitOut)

Run the prover in an interactive reduction. Returns the output statement and witness, and the transcript. See runWithLog for a version that additionally returns the log of the prover's oracle queries.

Equations

• One or more equations did not get rendered due to their size.

@[inline, specialize #[]]

def Prover.runWithLog {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (stmt : StmtIn) (wit : WitIn) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) ((pSpec.FullTranscript × StmtOut × WitOut) × (oSpec ++ₒ [pSpec.Challenge]ₒ).QueryLog)

Run the prover in an interactive reduction, logging all the queries made by the prover. Returns the transcript, the output statement and witness, and the log of the prover's oracle queries.

Note: this is just a wrapper around run that logs the queries made by the prover.

Equations

• Prover.runWithLog stmt wit prover = (OracleComp.simulateQ loggingOracle (Prover.run stmt wit prover)).run

@[simp]

theorem Prover.runWithLog_discard_log_eq_run {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (stmt : StmtIn) (wit : WitIn) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) : Prod.fst <$> runWithLog stmt wit prover = run stmt wit prover

@[reducible, inline, specialize #[]]

def Verifier.run {ι : Type} {oSpec : OracleSpec ι} {StmtIn StmtOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (stmt : StmtIn) (transcript : pSpec.FullTranscript) (verifier : Verifier oSpec StmtIn StmtOut pSpec) : OracleComp oSpec StmtOut

Run the (non-oracle) verifier in an interactive reduction. It takes in the input statement and the transcript, and return the output statement.

Equations

• Verifier.run stmt transcript verifier = verifier.verify stmt transcript

@[inline, specialize #[]]

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

Run the oracle verifier in the interactive protocol. Returns the verifier's output, including both the output statement and oracle statements, and the log of queries made by the verifier.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OracleVerifier.run_eq_run_verifier {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] {StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {n : ℕ} {pSpec : ProtocolSpec n} [Oₘ : (i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] {stmt : StmtIn} {oStmt : (i : ιₛᵢ) → OStmtIn i} {transcript : pSpec.FullTranscript} {verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec} : run stmt oStmt transcript verifier = Verifier.run (stmt, oStmt) transcript verifier.toVerifier

Running an oracle verifier then is equal to running its non-oracle counterpart

@[inline, specialize #[]]

def Reduction.run {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (stmt : StmtIn) (wit : WitIn) (reduction : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) ((pSpec.FullTranscript × StmtOut × WitOut) × StmtOut)

An execution of an interactive reduction on a given initial statement and witness. Consists of first running the prover, and then the verifier. Returns the full transcript, the output statement and witness from the prover, and the output statement from the verifier.

See Reduction.runWithLog for a version that additionally returns the logs of the prover's and the verifier's oracle queries.

Equations

• One or more equations did not get rendered due to their size.

@[inline, specialize #[]]

def Reduction.runWithLog {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (stmt : StmtIn) (wit : WitIn) (reduction : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) (((pSpec.FullTranscript × StmtOut × WitOut) × StmtOut) × (oSpec ++ₒ [pSpec.Challenge]ₒ).QueryLog × oSpec.QueryLog)

An execution of an interactive reduction on a given initial statement and witness. Consists of first running the prover, and then the verifier. Returns the full transcript, the output statement and witness from the prover, and the output statement from the verifier, along with the logs of the prover's and the verifier's oracle queries.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Reduction.runWithLog_discard_logs_eq_run {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} {stmt : StmtIn} {wit : WitIn} {reduction : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec} : Prod.fst <$> runWithLog stmt wit reduction = run stmt wit reduction

Logging the queries made by both parties do not change the output of the reduction

@[inline, specialize #[]]

def OracleReduction.run {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] {WitIn StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} [(i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] (stmt : StmtIn) (oStmt : (i : ιₛᵢ) → OStmtIn i) (wit : WitIn) (reduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) ((pSpec.FullTranscript × (StmtOut × ((i : ιₛₒ) → OStmtOut i)) × WitOut) × StmtOut × ((i : ιₛₒ) → OStmtOut i))

Run an interactive oracle reduction. Returns the full transcript, the output statement and witness, the log of all prover's oracle queries, and the log of all verifier's oracle queries to the prover's messages and to the shared oracle.

Equations

• One or more equations did not get rendered due to their size.

@[inline, specialize #[]]

def OracleReduction.runWithLog {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] {WitIn StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} [(i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] (stmt : StmtIn) (oStmt : (i : ιₛᵢ) → OStmtIn i) (wit : WitIn) (reduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) ((pSpec.FullTranscript × (StmtOut × ((i : ιₛₒ) → OStmtOut i)) × WitOut) × (StmtOut × ((i : ιₛₒ) → OStmtOut i)) × (oSpec ++ₒ [pSpec.Challenge]ₒ).QueryLog × oSpec.QueryLog)

Run an interactive oracle reduction. Returns the full transcript, the output statement and witness, the log of all prover's oracle queries, and the log of all verifier's oracle queries to the prover's messages and to the shared oracle.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OracleReduction.run_eq_run_reduction {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] {WitIn StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} [(i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] {stmt : StmtIn} {oStmt : (i : ιₛᵢ) → OStmtIn i} {wit : WitIn} {oracleReduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec} : run stmt oStmt wit oracleReduction = Reduction.run (stmt, oStmt) wit oracleReduction.toReduction

Running an oracle reduction is equal to running its non-oracle counterpart

@[simp]

theorem OracleReduction.runWithLog_eq_runWithLog_reduction {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] {WitIn StmtOut ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} [(i : pSpec.MessageIdx) → OracleInterface (pSpec.Message i)] {stmt : StmtIn} {oStmt : (i : ιₛᵢ) → OStmtIn i} {wit : WitIn} {oracleReduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec} : run stmt oStmt wit oracleReduction = Reduction.run (stmt, oStmt) wit oracleReduction.toReduction

Running an oracle reduction with logging of queries to the shared oracle is equal to running its non-oracle counterpart with logging of queries to the shared oracle

@[simp]

theorem Prover.runToRound_zero_of_prover_first {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {n : ℕ} {pSpec : ProtocolSpec n} (stmt : StmtIn) (wit : WitIn) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) : runToRound 0 stmt wit prover = pure (default, prover.input (stmt, wit))

@[simp]

theorem Reduction.id_run {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn : Type} (stmt : StmtIn) (wit : WitIn) : run stmt wit Reduction.id = pure ((default, stmt, wit), stmt)

Running the identity or trivial reduction results in the same input statement and witness, and empty transcript.

@[simp]

theorem Reduction.id_runWithLog {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn : Type} (stmt : StmtIn) (wit : WitIn) : runWithLog stmt wit Reduction.id = pure (((default, stmt, wit), stmt), [], [])

Running the identity or trivial reduction, with logging of queries to the shared oracle, results in the same input statement and witness, empty transcript, and empty query logs.

@[simp]

theorem OracleReduction.id_run {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] {WitIn : Type} (stmt : StmtIn) (oStmt : (i : ιₛᵢ) → OStmtIn i) (wit : WitIn) : run stmt oStmt wit OracleReduction.id = pure ((default, (stmt, oStmt), wit), stmt, oStmt)

Running the identity or trivial oracle reduction results in the same input statement, oracle statement, and witness.

@[simp]

theorem OracleReduction.id_runWithLog {ι : Type} {oSpec : OracleSpec ι} {StmtIn ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : (i : ιₛᵢ) → OracleInterface (OStmtIn i)] {WitIn : Type} (stmt : StmtIn) (oStmt : (i : ιₛᵢ) → OStmtIn i) (wit : WitIn) : runWithLog stmt oStmt wit OracleReduction.id = pure ((default, (stmt, oStmt), wit), (stmt, oStmt), [], [])

Running the identity or trivial oracle reduction results in the same input statement, oracle statement, and witness.

Simplification lemmas for protocols with a single message

@[simp]

theorem Prover.runToRound_one_of_prover_first {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {pSpec : ProtocolSpec 1} [pSpec.ProverOnly] (stmt : StmtIn) (wit : WitIn) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) : runToRound 1 stmt wit prover = have state := prover.input (stmt, wit); do let __discr ← (prover.sendMessage ⟨0, ⋯⟩ state).liftComp (oSpec ++ₒ [pSpec.Challenge]ₒ) match __discr with | (msg, state) => pure (fun (i : Fin ↑1) => match i with | ⟨0, isLt⟩ => msg, state)

@[simp]

theorem Prover.run_of_prover_first {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {pSpec : ProtocolSpec 1} [pSpec.ProverOnly] (stmt : StmtIn) (wit : WitIn) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) : run stmt wit prover = have state := prover.input (stmt, wit); do let __discr ← (prover.sendMessage ⟨0, ⋯⟩ state).liftComp (oSpec ++ₒ [pSpec.Challenge]ₒ) match __discr with | (msg, state) => do let ctxOut ← liftM (prover.output state) pure (fun (i : Fin 1) => match i with | ⟨0, isLt⟩ => msg, ctxOut)

theorem Reduction.run_of_prover_first {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} {pSpec : ProtocolSpec 1} [pSpec.ProverOnly] (stmt : StmtIn) (wit : WitIn) (reduction : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec) : run stmt wit reduction = have state := reduction.prover.input (stmt, wit); do let __discr ← (reduction.prover.sendMessage ⟨0, ⋯⟩ state).liftComp (oSpec ++ₒ [pSpec.Challenge]ₒ) match __discr with | (msg, state) => do let ctxOut ← liftM (reduction.prover.output state) have transcript : pSpec.FullTranscript := fun (i : Fin 1) => match i with | ⟨0, isLt⟩ => msg let stmtOut ← liftM (reduction.verifier.verify stmt transcript) pure ((transcript, ctxOut), stmtOut)