Semantics of Virtual (Oracle) Reductions

Sequential composition is usually not enough to represent oracle reductions in a modular way. We also need to formalize virtual oracle reductions, which lift reductions from one (virtual) context into the another (real) context.

This is what is meant when we informally say "apply so-and-so protocol to this quantity (derived from the input statement & witness)".

structure TransportStatement (StmtIn StmtOut StmtIn' StmtOut' : Type) : Type

• fStmtIn : StmtIn → StmtIn'
• fStmtOut : StmtIn × StmtOut' → StmtOut

structure TransportWitness (WitIn WitOut WitIn' WitOut' : Type) : Type

• fWitIn : WitIn → WitIn'
• fWitOut : WitIn × WitOut' → WitOut

structure TransportData (StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type) extends TransportStatement StmtIn StmtOut StmtIn' StmtOut', TransportWitness WitIn WitOut WitIn' WitOut' : Type

• fStmtIn : StmtIn → StmtIn'
• fStmtOut : StmtIn × StmtOut' → StmtOut
• fWitIn : WitIn → WitIn'
• fWitOut : WitIn × WitOut' → WitOut

structure TransportStatementInv (StmtIn StmtOut StmtIn' StmtOut' : Type) : Type

• fStmtInInv : StmtOut × StmtIn' → StmtIn
• fStmtOutInv : StmtOut → StmtOut'

structure TransportWitnessInv (WitIn WitOut WitIn' WitOut' : Type) : Type

• fWitInInv : WitOut × WitIn' → WitIn
• fWitOutInv : WitOut → WitOut'

structure TransportDataInv (StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type) extends TransportStatementInv StmtIn StmtOut StmtIn' StmtOut', TransportWitnessInv WitIn WitOut WitIn' WitOut' : Type

• fStmtInInv : StmtOut × StmtIn' → StmtIn
• fStmtOutInv : StmtOut → StmtOut'
• fWitInInv : WitOut × WitIn' → WitIn
• fWitOutInv : WitOut → WitOut'

structure TransportDataComplete (StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type) (relIn : StmtIn → WitIn → Prop) (relIn' : StmtIn' → WitIn' → Prop) (relOut : StmtOut → WitOut → Prop) (relOut' : StmtOut' → WitOut' → Prop) extends TransportData StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type

Conditions for the transformation to preserve completeness

NOTE: this is not the correct condition for now (see example)

• fStmtIn : StmtIn → StmtIn'
• fStmtOut : StmtIn × StmtOut' → StmtOut
• fWitIn : WitIn → WitIn'
• fWitOut : WitIn × WitOut' → WitOut
• relIn_implies (stmtIn : StmtIn) (witIn : WitIn) : relIn stmtIn witIn → relIn' (self.fStmtIn stmtIn) (self.fWitIn witIn)
• relOut_implied_by (stmtIn : StmtIn) (witIn : WitIn) (stmtOut' : StmtOut') (witOut' : WitOut') : relIn stmtIn witIn → relOut' stmtOut' witOut' → relOut (self.fStmtOut (stmtIn, stmtOut')) (self.fWitOut (witIn, witOut'))

structure TransportDataSound (StmtIn StmtOut StmtIn' StmtOut' : Type) (langIn : Set StmtIn) (langOut : Set StmtOut) (langIn' : Set StmtIn') (langOut' : Set StmtOut') extends TransportStatement StmtIn StmtOut StmtIn' StmtOut', TransportStatementInv StmtIn StmtOut StmtIn' StmtOut' : Type

• fStmtIn : StmtIn → StmtIn'
• fStmtOut : StmtIn × StmtOut' → StmtOut
• fStmtInInv : StmtOut × StmtIn' → StmtIn
• fStmtOutInv : StmtOut → StmtOut'

structure TransportDataKnowledgeSound (StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type) (relIn : StmtIn → WitIn → Prop) (relIn' : StmtIn' → WitIn' → Prop) (relOut : StmtOut → WitOut → Prop) (relOut' : StmtOut' → WitOut' → Prop) extends TransportData StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut', TransportDataInv StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type

• fStmtIn : StmtIn → StmtIn'
• fStmtOut : StmtIn × StmtOut' → StmtOut
• fWitIn : WitIn → WitIn'
• fWitOut : WitIn × WitOut' → WitOut
• fStmtInInv : StmtOut × StmtIn' → StmtIn
• fStmtOutInv : StmtOut → StmtOut'
• fWitInInv : WitOut × WitIn' → WitIn
• fWitOutInv : WitOut → WitOut'

def Prover.transport {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type} (data : TransportData StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut') (P : Prover pSpec oSpec StmtIn' WitIn' StmtOut' WitOut') : Prover pSpec oSpec StmtIn WitIn StmtOut WitOut

How does the prover change? Only in input & output, and keep around the input statement & witness

Equations

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

def Verifier.transport {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} {oSpec : OracleSpec ι} {StmtIn StmtOut StmtIn' StmtOut' : Type} (data : TransportStatement StmtIn StmtOut StmtIn' StmtOut') (V : Verifier pSpec oSpec StmtIn' StmtOut') : Verifier pSpec oSpec StmtIn StmtOut

Equations

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

def Reduction.transport {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type} (data : TransportData StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut') (R : Reduction pSpec oSpec StmtIn' WitIn' StmtOut' WitOut') : Reduction pSpec oSpec StmtIn WitIn StmtOut WitOut

Equations

• Reduction.transport data R = { prover := Prover.transport data R.prover, verifier := Verifier.transport data.toTransportStatement R.verifier }

def StraightlineExtractor.transport {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type} (data : TransportData StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut') (dataInv : TransportDataInv StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut') (E : Reduction.StraightlineExtractor) : Reduction.StraightlineExtractor

Equations

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

theorem Prover.run_transport {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} [DecidableEq ι] {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] [oSpec.FiniteRange] {data : TransportData StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut'} {stmtIn : StmtIn} {witIn : WitIn} (P : Prover pSpec oSpec StmtIn' WitIn' StmtOut' WitOut') : run stmtIn witIn (transport data P) = do let __discr ← run (data.fStmtIn stmtIn) (data.fWitIn witIn) P match __discr with | (stmtOut, witOut, fullTranscript) => pure (data.fStmtOut (stmtIn, stmtOut), data.fWitOut (witIn, witOut), fullTranscript)

theorem Reduction.run_transport {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} [DecidableEq ι] {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] [oSpec.FiniteRange] {data : TransportData StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut'} {stmtIn : StmtIn} {witIn : WitIn} (R : Reduction pSpec oSpec StmtIn' WitIn' StmtOut' WitOut') : run stmtIn witIn (transport data R) = do let __discr ← run (data.fStmtIn stmtIn) (data.fWitIn witIn) R match __discr with | ((prvStmtOut, witOut), verStmtOut, fullTranscript) => pure ((data.fStmtOut (stmtIn, prvStmtOut), data.fWitOut (witIn, witOut)), data.fStmtOut (stmtIn, verStmtOut), fullTranscript)

theorem Reduction.runWithLog_transport {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} [DecidableEq ι] {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] [oSpec.FiniteRange] {data : TransportData StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut'} {stmtIn : StmtIn} {witIn : WitIn} (R : Reduction pSpec oSpec StmtIn' WitIn' StmtOut' WitOut') : runWithLog stmtIn witIn (transport data R) = do let __discr ← runWithLog (data.fStmtIn stmtIn) (data.fWitIn witIn) R match __discr with | ((prvStmtOut, witOut), verStmtOut, fullTranscript, queryLog) => pure ((data.fStmtOut (stmtIn, prvStmtOut), data.fWitOut (witIn, witOut)), data.fStmtOut (stmtIn, verStmtOut), fullTranscript, queryLog)

theorem Reduction.transport_completeness {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} [DecidableEq ι] {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] [oSpec.FiniteRange] {relIn : StmtIn → WitIn → Prop} {relOut : StmtOut → WitOut → Prop} {relIn' : StmtIn' → WitIn' → Prop} {relOut' : StmtOut' → WitOut' → Prop} {completenessError : NNReal} (data : TransportDataComplete StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' relIn relIn' relOut relOut') (R : Reduction pSpec oSpec StmtIn' WitIn' StmtOut' WitOut') (h : completeness relIn' relOut' R completenessError) : completeness relIn relOut (transport data.toTransportData R) completenessError

Informally, if (stmtIn, witIn) ∈ relIn, we want (stmtIn', witIn') ∈ relIn'. Using the completeness guarantee, we get that (stmtOut', witOut') ∈ relOut'. From these, we need to deduce that (stmtOut, witOut) ∈ relOut.

theorem Reduction.transport_soundness {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} [DecidableEq ι] {oSpec : OracleSpec ι} {StmtIn StmtOut StmtIn' StmtOut' : Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] [oSpec.FiniteRange] {langIn : Set StmtIn} {langOut : Set StmtOut} {langIn' : Set StmtIn'} {langOut' : Set StmtOut'} {soundnessError : NNReal} (data : TransportDataSound StmtIn StmtOut StmtIn' StmtOut' langIn langOut langIn' langOut') (V : Verifier pSpec oSpec StmtIn' StmtOut') (h : soundness langIn' langOut' V soundnessError) : soundness langIn langOut (Verifier.transport data.toTransportStatement V) soundnessError

theorem Reduction.transport_knowledgeSoundness {n : ℕ} {pSpec : ProtocolSpec n} {ι : Type} [DecidableEq ι] {oSpec : OracleSpec ι} {StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' : Type} [(i : pSpec.ChallengeIndex) → VCVCompatible (pSpec.Challenge i)] [oSpec.FiniteRange] {relIn : StmtIn → WitIn → Prop} {relOut : StmtOut → WitOut → Prop} {relIn' : StmtIn' → WitIn' → Prop} {relOut' : StmtOut' → WitOut' → Prop} {soundnessError : NNReal} (data : TransportDataKnowledgeSound StmtIn WitIn StmtOut WitOut StmtIn' WitIn' StmtOut' WitOut' relIn relIn' relOut relOut') (V : Verifier pSpec oSpec StmtIn' StmtOut') (h : knowledgeSoundness relIn' relOut' V soundnessError) : knowledgeSoundness relIn relOut (Verifier.transport data.toTransportStatement V) soundnessError

def StmtIn : Type

Equations

• StmtIn = (Polynomial ℤ × Polynomial ℤ × ℤ)

def StmtIn' : Type

Equations

• StmtIn' = (Polynomial ℤ × ℤ)

def relIn : StmtIn → Unit → Prop

Equations

• relIn (p, q, t) x✝ = (∑ x ∈ {0, 1}, Polynomial.eval x (p * q) = t)

def relIn' : StmtIn' → Unit → Prop

Equations

• relIn' (f, t) x✝ = (∑ x ∈ {0, 1}, Polynomial.eval x f = t)

def StmtOut : Type

Equations

• StmtOut = (Polynomial ℤ × Polynomial ℤ × ℤ × ℤ)

def StmtOut' : Type

Equations

• StmtOut' = (Polynomial ℤ × ℤ × ℤ)

def relOut : StmtOut → Unit → Prop

Equations

• relOut (p, q, t, r) x✝ = (Polynomial.eval r (p * q) = t)

def relOut' : StmtOut' → Unit → Prop

Equations

• relOut' (f, t, r) x✝ = (Polynomial.eval r f = t)

def data : TransportData StmtIn Unit StmtOut Unit StmtIn' Unit StmtOut' Unit

Equations

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

def dataComplete : TransportDataComplete StmtIn Unit StmtOut Unit StmtIn' Unit StmtOut' Unit relIn relIn' relOut relOut'

Equations

• dataComplete = { toTransportData := data, relIn_implies := dataComplete.proof_1, relOut_implied_by := dataComplete.proof_2 }