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

@[inline, specialize #[]]

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

Run the prover in an interactive reduction up to round index i. Returns the transcript up to that round, and the prover's state after that round.

Equations

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

@[inline, specialize #[]]

def Prover.runWithLogToRound {n : ℕ} {ι : Type} {pSpec : ProtocolSpec n} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] (i : Fin (n + 1)) (stmt : StmtIn) (wit : WitIn) (prover : Prover pSpec oSpec StmtIn WitIn StmtOut WitOut) : 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.

Equations

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

@[inline, specialize #[]]

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

Run the prover in an interactive reduction. Returns the output statement and witness, and the transcript. See Prover.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 {n : ℕ} {ι : Type} {pSpec : ProtocolSpec n} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] (stmt : StmtIn) (wit : WitIn) (prover : Prover pSpec oSpec StmtIn WitIn StmtOut WitOut) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) (StmtOut × WitOut × pSpec.FullTranscript × (oSpec ++ₒ [pSpec.Challenge]ₒ).QueryLog)

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

Equations

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

@[reducible, inline, specialize #[]]

def Verifier.run {n : ℕ} {ι : Type} {pSpec : ProtocolSpec n} {oSpec : OracleSpec ι} {StmtIn StmtOut : Type} (stmt : StmtIn) (transcript : pSpec.FullTranscript) (verifier : Verifier pSpec oSpec StmtIn StmtOut) : 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 along with the log of oracle queries made by the veirifer.

Equations

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

@[inline, specialize #[]]

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

Run the oracle verifier in the interactive protocol. Returns the verifier's output 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 {n : ℕ} {ι : Type} {pSpec : ProtocolSpec n} {oSpec : OracleSpec ι} {StmtIn StmtOut ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : (i : ιₛᵢ) → ToOracle (OStmtIn i)] {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} [(i : pSpec.MessageIndex) → ToOracle (pSpec.Message i)] {stmt : StmtIn} {transcript : pSpec.FullTranscript} {oStmt : (i : ιₛᵢ) → OStmtIn i} {verifier : OracleVerifier pSpec oSpec StmtIn StmtOut OStmtIn OStmtOut} : run stmt oStmt transcript verifier = Prod.fst <$> Verifier.run (stmt, oStmt) transcript verifier.toVerifier

Running an oracle verifier then discarding the query list is equivalent to running a non-oracle verifier

@[inline, specialize #[]]

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

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 output statement and witness, and the full transcript.

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 {n : ℕ} {ι : Type} {pSpec : ProtocolSpec n} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] (stmt : StmtIn) (wit : WitIn) (reduction : Reduction pSpec oSpec StmtIn WitIn StmtOut WitOut) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) ((StmtOut × WitOut) × StmtOut × pSpec.FullTranscript × (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 output statement and witness, the full transcript, and 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_eq_run {n : ℕ} {ι : Type} {pSpec : ProtocolSpec n} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] {stmt : StmtIn} {wit : WitIn} {reduction : Reduction pSpec oSpec StmtIn WitIn StmtOut WitOut} : (fun (x : (StmtOut × WitOut) × StmtOut × pSpec.FullTranscript × (oSpec ++ₒ [pSpec.Challenge]ₒ).QueryLog × oSpec.QueryLog) => match x with | (prvOutput, witOut, transcript, fst, snd) => (prvOutput, witOut, transcript)) <$> 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 {n : ℕ} {ι : Type} {pSpec : ProtocolSpec n} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : (i : ιₛᵢ) → ToOracle (OStmtIn i)] {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] [(i : pSpec.MessageIndex) → ToOracle (pSpec.Message i)] (stmt : StmtIn) (wit : WitIn) (oStmt : (i : ιₛᵢ) → OStmtIn i) (reduction : OracleReduction pSpec oSpec StmtIn WitIn StmtOut WitOut OStmtIn OStmtOut) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) (((StmtOut × ((i : ιₛₒ) → OStmtOut i)) × WitOut) × StmtOut × pSpec.FullTranscript × (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 Prover.runToRound_zero_of_prover_first {n : ℕ} {ι : Type} {pSpec : ProtocolSpec n} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut : Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] (stmt : StmtIn) (wit : WitIn) (prover : Prover pSpec oSpec StmtIn WitIn StmtOut WitOut) : runToRound 0 stmt wit prover = pure (default, prover.input stmt wit)

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 pSpec oSpec StmtIn WitIn StmtOut WitOut) : runToRound 1 stmt wit prover = let 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 pSpec oSpec StmtIn WitIn StmtOut WitOut) : run stmt wit prover = let state := prover.input stmt wit; do let __discr ← (prover.sendMessage ⟨0, ⋯⟩ state).liftComp (oSpec ++ₒ [pSpec.Challenge]ₒ) match __discr with | (msg, state) => match prover.output state with | (stmtOut, witOut) => pure (stmtOut, witOut, fun (i : Fin 1) => match i with | ⟨0, isLt⟩ => msg)

@[simp]

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 pSpec oSpec StmtIn WitIn StmtOut WitOut) : run stmt wit reduction = let state := reduction.prover.input stmt wit; do let __discr ← (reduction.prover.sendMessage ⟨0, ⋯⟩ state).liftComp (oSpec ++ₒ [pSpec.Challenge]ₒ) match __discr with | (msg, state) => match reduction.prover.output state with | (prvStmtOut, witOut) => let transcript := fun (i : Fin 1) => match i with | ⟨0, isLt⟩ => msg; do let stmtOut ← liftM (reduction.verifier.verify stmt transcript) pure ((prvStmtOut, witOut), stmtOut, transcript)