Rewinding Knowledge Soundness

This file defines rewinding knowledge soundness for (oracle) reductions.

TODO: under development

def Extractor.OracleSpec.proverOracle (StmtIn : Type) {n : ℕ} (pSpec : ProtocolSpec n) : OracleSpec pSpec.MessageIdx

The oracle interface to call the prover as a black box

Equations

• Extractor.OracleSpec.proverOracle StmtIn pSpec i = (StmtIn × ProtocolSpec.Transcript (↑i).castSucc pSpec, pSpec.Message i)

structure Extractor.Rewinding {ι : Type} (oSpec : OracleSpec ι) (StmtIn StmtOut WitIn WitOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) : Type 1

• ExtState : Type

  The state of the extractor

• simChallenge : SimOracle.Stateful [pSpec.Challenge]ₒ [pSpec.Challenge]ₒ self.ExtState

  Simulate challenge queries for the prover

• simOracle : SimOracle.Stateful oSpec oSpec self.ExtState

  Simulate oracle queries for the prover

• runExt : StmtOut → WitOut → StmtIn → StateT self.ExtState (OracleComp (OracleSpec.proverOracle StmtIn pSpec)) WitIn

  Run the extractor with the prover's oracle interface, allowing for calling the prover multiple times